Supporting fix/cofix in Ltac pattern-matching (wish #7092).

This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.

1 files changed, 70 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/7092.v b/test-suite/bugs/closed/7092.v
new file mode 100644
index 000000000..d90de8b93
--- /dev/null
+++ b/test-suite/bugs/closed/7092.v
@@ -0,0 +1,70 @@
+(* Examples matching fix/cofix in Ltac pattern-matching *)
+
+Goal True.
+lazymatch (eval cbv delta [Nat.add] in Nat.add) with
+| (fix F (n : nat) (v : ?A) {struct n} : @?P n v
+     := match n with
+        | O => @?O_case v
+        | S n' => @?S_case n' v F
+        end)
+    =>
+         unify A nat;
+         unify P (fun _ _ : nat => nat);
+         unify O_case (fun v : nat => v);
+         unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat)
+                       => S (add p m))
+  end.
+Abort.
+
+Fixpoint f l n := match n with 0 => 0 | S n => g n (cons n l) end
+with g n l := match n with 0 => 1 | S n => f (cons 0 l) n end.
+
+Goal True.
+
+lazymatch (eval cbv delta [f] in f) with
+| fix myf (l : ?L) (n : ?N) {struct n} : nat :=
+    match n as _ with
+    | 0 => ?Z
+    | S n0 => @?S myf myg n0 l
+    end
+  with myg (n' : ?N') (l' : ?L') {struct n'} : nat :=
+    match n' as _ with
+    | 0 => ?Z'
+    | S n0' => @?S' myf myg n0' l'
+    end
+  for myf =>
+    unify L (list nat);
+    unify L' (list nat);
+    unify N nat;
+    unify N' nat;
+    unify Z 0;
+    unify Z' 1;
+    unify S (fun (f : L -> N -> nat) (g : N -> L -> nat) n l => g n (cons n l));
+    unify S' (fun (f : L -> N -> nat) (g : N -> L -> nat) (n:N) l => f (cons 0 l) n)
+end.
+
+Abort.
+
+CoInductive S1 := C1 : nat -> S2 -> S1 with S2 := C2 : bool -> S1 -> S2.
+
+CoFixpoint f' n l := C1 n (g' (cons n l) n n)
+with g' l n p := C2 true (f' (S n) l).
+
+Goal True.
+
+lazymatch (eval cbv delta [f'] in f') with
+| cofix myf (n : ?N) (l : ?L) : ?T := @?X n g l
+  with g (l' : ?L') (n' : ?N') (p' : ?N'') : ?T' := @?X' n' myf l'
+  for myf =>
+    unify L (list nat);
+    unify L' (list nat);
+    unify N nat;
+    unify N' nat;
+    unify N'' nat;
+    unify T S1;
+    unify T' S2;
+    unify X (fun n g l => C1 n (g (cons n l) n n));
+    unify X' (fun n f (l : list nat) => C2 true (f (S n) l))
+end.
+
+Abort.