# Obligation Tactic := intros. results in the Program Fixpoint with measure not being defined

I have a Program Fixpoint with measure for which I have proved all obligations. When I try to check it, it fails:

I have narrowed the error to the use of a non default tactic to prove obligations. In the code below, the first Program is defined. Once I choose a non default tactic to prove Obligations, the Program doesn't get defined even though there are no Obligation's left to prove. I would expect trivial_program_fixpoint2 to be defined after Qed.

I have looked in the documentation but I don't see anything that suggests that using a tactic different than default would change what I am seeing.

Coq version used:

The Coq Proof Assistant, version 8.15+alpha compiled with OCaml 4.09.1

Below is code to reproduce the problem.

From Coq Require Export Arith.
Require Import Program.Wf.

Program Fixpoint trivial_program_fixpoint (n : nat) {measure n}: nat :=
match n with
0 => 0
| m => m
end.
Check trivial_program_fixpoint.

Obligation Tactic := intros.

Program Fixpoint trivial_program_fixpoint2 (n : nat) {measure n}: nat :=
match n with
0 => 0
| m => m
end.
Next Obligation.
intuition. discriminate.
Qed.
Check trivial_program_fixpoint2.


Your second Program Fixpoint produced two obligations.

trivial_program_fixpoint2 has type-checked, generating 2 obligations

Solving obligations automatically...

2 obligations remaining

• Thanks. I thought Qed was used when no obligations are left. Jun 10 at 13:42
• @RolandCoeurjoly Qed is accepted when no goals are left. The obligations generated by Program work a little differently. I don't know why this is. One consequence is that each solved obligation becomes a defined object in its own right, and one can choose whether to close them with Defined or Qed. Jun 10 at 15:16
• Program is different (obligations are not generated as subgoals) because it lets you choose whether to make the obligations transparent or not.
– HTNW
Jun 12 at 11:40