Use multiple statements to implement interactive fixpoints

test-suite/output/Fixpoint.out

@@ -35,3 +35,62 @@ File "./output/Fixpoint.v", line 75, characters 0-48:
 Warning: Not a fully mutually defined cofixpoint
 (a2 and a1 are not mutually dependent).
  [non-full-mutual,fixpoints,default]
+File "./output/Fixpoint.v", line 91, characters 2-15:
+The command has indeed failed with message:
+Recursive definition of foo and bar is ill-formed.
+As a mutual fixpoint:
+Not enough abstractions in the definition.
+The 1st recursive definition is: "?Goal".
+The 2nd recursive definition is: "?Goal0".
+The condition holds up to here.
+File "./output/Fixpoint.v", line 96, characters 6-19:
+The command has indeed failed with message:
+Recursive definition of foo and bar is ill-formed.
+As a mutual fixpoint decreasing on the 1st argument of foo and
+1st argument of bar:
+Recursive call to bar has principal argument equal to 
+"0" instead of
+a subterm of "n".
+As a mutual fixpoint decreasing on the 1st argument of foo and
+2nd argument of bar:
+Recursive call to bar has principal argument equal to 
+"0" instead of
+a subterm of "n".
+As a mutual fixpoint decreasing on the 2nd argument of foo and
+1st argument of bar:
+Recursive call to bar has principal argument equal to 
+"0" instead of
+a subterm of "m".
+As a mutual fixpoint decreasing on the 2nd argument of foo and
+2nd argument of bar:
+Recursive call to bar has principal argument equal to 
+"0" instead of a subterm of "m".
+The 1st recursive definition is:
+"fun n m : nat =>
+ match n with
+ | 0 => bar 0 0
+ | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0
+ end".
+The 2nd recursive definition is: "fun n m : nat => ?Goal".
+The condition holds up to here.
+The condition holds up to here.
+The condition holds up to here.
+The condition holds up to here.
+File "./output/Fixpoint.v", line 123, characters 6-19:
+The command has indeed failed with message:
+Recursive definition of foo' and bar' is ill-formed.
+As a mutual fixpoint decreasing on the 1st argument of foo' and
+1st argument of bar':
+Fixpoints on proof irrelevant inductive types should produce proof irrelevant
+values.
+As a mutual fixpoint decreasing on the 1st argument of foo' and
+2nd argument of bar':
+Recursive call to bar' has principal argument equal to 
+"0" instead of a subterm of "n".
+The 1st recursive definition is:
+"fun (n : nat) (m : Prop) =>
+ match n with
+ | 0 => bar' SI 0
+ | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0
+ end".
+The 2nd recursive definition is: "fun (n : STrue) (m : nat) => ?Goal".

test-suite/output/Fixpoint.v

@@ -80,3 +80,47 @@ with b2 := b1.
 *)
 
 End Recursivity.
+
+Module Guard.
+
+Open Scope nat_scope.
+
+Lemma foo : nat -> nat -> bool
+with bar : nat -> nat -> bool.
+Proof.
+  Fail Guarded. (* not enough abstractions in the definition *)
+  all:intros n m.
+  Guarded.
+  - destruct n as [|n].
+    + exact (bar 0 0).
+      Fail Guarded. (* failure is correct here *)
+Abort.
+
+Lemma foo : nat -> nat -> bool
+with bar : nat -> nat -> bool.
+Proof.
+  all:intros n m.
+  - destruct n as [|n].
+    + exact true.
+    + Guarded.
+      exact (bar m n).
+  - Guarded.
+    destruct m as [|m].
+    + exact false.
+    + exact (foo m n).
+      Guarded.
+Defined.
+
+Inductive STrue : SProp := SI.
+
+Lemma foo' : nat -> Prop -> bool
+with bar' : STrue -> nat -> bool.
+Proof.
+  all:intros n m.
+  - destruct n as [|n].
+    Guarded.
+    + exact (bar' SI 0).
+      Fail Guarded.
+Abort.
+
+End Guard.

vernac/comFixpoint.ml

@@ -564,20 +564,21 @@ let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ?
       let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~opaque:false ~body ~uctx ?using obls in
       Some pm, None
     | _ ->
+      let possible_guard = (possible_guard, fixrs) in
       Some (Declare.Obls.add_mutual_definitions ~pm ~cinfo ~info ~opaque:false ~uctx ~bodies ~possible_guard ?using obls), None)
   | None ->
     try
       let bodies = List.map Option.get bodies in
       let uctx = Evd.evar_universe_context sigma in
       (* All bodies are defined *)
+      let possible_guard = (possible_guard, fixrs) in
       let _ : GlobRef.t list =
-        Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx
-          ~possible_guard ~bodies:(bodies,fixrs) ?using ()
+        Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx ~possible_guard ~bodies ?using ()
       in
       None, None
     with Option.IsNone ->
       (* At least one undefined body *)
       Evd.check_univ_decl_early ~poly ~with_obls:false sigma udecl (Option.List.flatten bodies @ fixtypes);
-      let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo
-          ~bodies ~possible_guard ?using sigma in
+      let possible_guard = (possible_guard, fixrs) in
+      let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma in
       None, Some lemma