Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)

11 files changed, 355 insertions, 124 deletions

diff --git a/CHANGES b/CHANGES
index d982e0af7..37d9d3680 100644
--- a/CHANGES
+++ b/CHANGES
@@ -11,6 +11,10 @@ Vernacular Commands
 - Removed deprecated commands Arguments Scope and Implicit Arguments
   (not the option). Use the Arguments command instead.
 
+Tactic language
+
+- Support for fix/cofix added in Ltac "match" and "lazymatch".
+
 Changes from 8.7.2 to 8.8+beta1
 ===============================
 
diff --git a/clib/cArray.ml b/clib/cArray.ml
index b6c033f6d..5eb20bc16 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -41,6 +41,8 @@ sig
     ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left3 :
     ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a
+  val fold_left4 :
+    ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a
   val fold_left2_i :
     (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
@@ -267,6 +269,16 @@ let fold_left3 f a v1 v2 v3 =
     invalid_arg "Array.fold_left2";
   fold a 0
 
+let fold_left4 f a v1 v2 v3 v4 =
+  let lv1 = Array.length v1 in
+  let rec fold a n =
+    if n >= lv1 then a
+    else fold (f a (uget v1 n) (uget v2 n) (uget v3 n) (uget v4 n)) (succ n)
+  in
+  if Array.length v2 <> lv1 || Array.length v3 <> lv1 || Array.length v4 <> lv1 then
+    invalid_arg "Array.fold_left4";
+  fold a 0
+
 let fold_left_from n f a v =
   let len = Array.length v in
   let () = if n < 0 then invalid_arg "Array.fold_left_from" in
diff --git a/clib/cArray.mli b/clib/cArray.mli
index 97038b0ac..f4f60f8aa 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -66,6 +66,8 @@ sig
     ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left3 :
     ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a
+  val fold_left4 :
+    ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a
   val fold_left2_i :
     (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19444988b..48ddd9496 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -14,7 +14,6 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Constr
 open Termops
 open Libnames
 open Globnames
@@ -1223,8 +1222,36 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
-  | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
-  | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+  | PFix ((ln,i),(lna,tl,bl)) ->
+     let def_avoid, def_env, lfi =
+       Array.fold_left
+         (fun (avoid, env, l) na ->
+           let id = Namegen.next_name_away na avoid in
+           (Id.Set.add id avoid, Name id :: env, id::l))
+      (avoid, env, []) lna in
+     let n = Array.length tl in
+     let v = Array.map3
+               (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
+    bl tl ln in
+     GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+  | PCoFix (ln,(lna,tl,bl)) ->
+     let def_avoid, def_env, lfi =
+       Array.fold_left
+         (fun (avoid, env, l) na ->
+           let id = Namegen.next_name_away na avoid in
+           (Id.Set.add id avoid, Name id :: env, id::l))
+         (avoid, env, []) lna in
+     let ntys = Array.length tl in
+     let v = Array.map2
+               (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t))
+               bl tl in
+     GRec(GCoFix ln,Array.of_list (List.rev lfi),
+          Array.map (fun (bl,_,_) -> bl) v,
+          Array.map (fun (_,_,ty) -> ty) v,
+          Array.map (fun (_,bd,_) -> bd) v)
   | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
diff --git a/intf/pattern.ml b/intf/pattern.ml
index af2347674..76367b612 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -10,7 +10,6 @@
 
 open Names
 open Globnames
-open Constr
 open Misctypes
 
 (** {5 Patterns} *)
@@ -37,8 +36,8 @@ type constr_pattern =
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of case_info_pattern * constr_pattern * constr_pattern *
       (int * bool list * constr_pattern) list (** index of constructor, nb of args *)
-  | PFix of fixpoint
-  | PCoFix of cofixpoint
+  | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
+  | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
 
 (** Nota : in a [PCase], the array of branches might be shorter than
     expected, denoting the use of a final "_ => _" branch *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 888c76e3d..89d490a41 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -183,9 +183,36 @@ let push_binder na1 na2 t ctx =
      Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in
   (na1, id2, t) :: ctx
 
-let to_fix (idx, (nas, cs, ts)) =
-  let inj = EConstr.of_constr in
-  (idx, (nas, Array.map inj cs, Array.map inj ts))
+(* This is an optimization of the main pattern-matching which shares
+   the longest common prefix of the body and type of a fixpoint. The
+   only practical effect at the time of writing is in binding variable
+   names: these variable names must be bound only once since the user
+   view at a fix displays only a (maximal) shared common prefix *)
+
+let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 =
+  match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with
+  | PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') ->
+     let ctx = push_binder na1 na2 c2 ctx in
+     let ctx' = push_binder na1 na2' c2' ctx' in
+     let env = EConstr.push_rel (LocalAssum (na2,c2)) env in
+     let subst = sorec ctx env subst c1 c2 in
+     let subst = sorec ctx env subst c1' c2' in
+     let subst = add_binders na1 na2 binding_vars subst in
+     match_under_common_fix_binders sorec sigma binding_vars
+       ctx ctx' env env' subst t1' t2' b1' b2'
+  | PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) ->
+     let ctx = push_binder na1 na2 u2 ctx in
+     let ctx' = push_binder na1 na2' u2' ctx' in
+     let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in
+     let subst = sorec ctx env subst c1 c2 in
+     let subst = sorec ctx env subst c1' c2' in
+     let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in
+     let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in
+     let subst = add_binders na1 na2 binding_vars subst in
+     match_under_common_fix_binders sorec sigma binding_vars
+       ctx ctx' env env' subst t1 t2 b1 b2
+  | _ ->
+     sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2
 
 let merge_binding sigma allow_bound_rels ctx n cT subst =
   let c = match ctx with
@@ -364,8 +391,20 @@ let matches_core env sigma allow_bound_rels
 	  let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
 	  List.fold_left chk_branch chk_head br1
 
-      |	PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst
-      |	PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
+      |	PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2))
+           when Array.equal Int.equal ln1 ln2 && i1 = i2 ->
+          let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
+          let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
+          let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
+          Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
+
+      |	PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2))
+           when i1 = i2 ->
+          let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
+          let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
+          let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
+          Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
+
       | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
          Array.fold_left2 (sorec ctx env) subst args1 args2
       | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 587892141..bb563220b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -501,6 +501,97 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let eqnl = detype_eqns constructs constagsl bl in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
+let rec share_names detype n l avoid env sigma c t =
+  match EConstr.kind sigma c, EConstr.kind sigma t with
+    (* factorize even when not necessary to have better presentation *)
+    | Lambda (na,t,c), Prod (na',t',c') ->
+        let na = match (na,na') with
+            Name _, _ -> na
+          | _, Name _ -> na'
+          | _ -> na in
+        let t' = detype avoid env sigma t in
+        let id = next_name_away na avoid in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
+        share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+    (* May occur for fix built interactively *)
+    | LetIn (na,b,t',c), _ when n > 0 ->
+        let t'' = detype avoid env sigma t' in
+        let b' = detype avoid env sigma b in
+        let id = next_name_away na avoid in
+        let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
+        share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
+    (* Only if built with the f/n notation or w/o let-expansion in types *)
+    | _, LetIn (_,b,_,t) when n > 0 ->
+        share_names detype n l avoid env sigma c (subst1 b t)
+    (* If it is an open proof: we cheat and eta-expand *)
+    | _, Prod (na',t',c') when n > 0 ->
+        let t'' = detype avoid env sigma t' in
+        let id = next_name_away na' avoid in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
+        let appc = mkApp (lift 1 c,[|mkRel 1|]) in
+        share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
+    (* If built with the f/n notation: we renounce to share names *)
+    | _ ->
+        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+        let c = detype avoid env sigma c in
+        let t = detype avoid env sigma t in
+        (List.rev l,c,t)
+
+let rec share_pattern_names detype n l avoid env sigma c t =
+  let open Pattern in
+  if n = 0 then
+    let c = detype avoid env sigma c in
+    let t = detype avoid env sigma t in
+    (List.rev l,c,t)
+  else match c, t with
+    | PLambda (na,t,c), PProd (na',t',c') ->
+        let na = match (na,na') with
+            Name _, _ -> na
+          | _, Name _ -> na'
+          | _ -> na in
+        let t' = detype avoid env sigma t in
+        let id = next_name_away na avoid in
+        let avoid = Id.Set.add id avoid in
+        let env = Name id :: env in
+        share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+    | _ ->
+        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+        let c = detype avoid env sigma c in
+        let t = detype avoid env sigma t in
+        (List.rev l,c,t)
+
+let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
+  let def_avoid, def_env, lfi =
+    Array.fold_left2
+      (fun (avoid, env, l) na ty ->
+         let id = next_name_away na avoid in
+         (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+      (avoid, env, []) names tys in
+  let n = Array.length tys in
+  let v = Array.map3
+    (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t))
+    bodies tys vn in
+  GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+
+let detype_cofix detype avoid env sigma n (names,tys,bodies) =
+  let def_avoid, def_env, lfi =
+    Array.fold_left2
+      (fun (avoid, env, l) na ty ->
+         let id = next_name_away na avoid in
+         (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+      (avoid, env, []) names tys in
+  let ntys = Array.length tys in
+  let v = Array.map2
+    (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t))
+    bodies tys in
+  GRec(GCoFix n,Array.of_list (List.rev lfi),
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+
 let detype_universe sigma u =
   let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
   Univ.Universe.map fn u
@@ -655,76 +746,8 @@ and detype_r d flags avoid env sigma t =
 	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
           p c bl
-    | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef
-    | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef
-
-and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
-  let def_avoid, def_env, lfi =
-    Array.fold_left2
-      (fun (avoid, env, l) na ty ->
-	 let id = next_name_away na avoid in
-	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
-      (avoid, env, []) names tys in
-  let n = Array.length tys in
-  let v = Array.map3
-    (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t))
-    bodies tys vn in
-  GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
-       Array.map (fun (bl,_,_) -> bl) v,
-       Array.map (fun (_,_,ty) -> ty) v,
-       Array.map (fun (_,bd,_) -> bd) v)
-
-and detype_cofix d flags avoid env sigma n (names,tys,bodies) =
-  let def_avoid, def_env, lfi =
-    Array.fold_left2
-      (fun (avoid, env, l) na ty ->
-	 let id = next_name_away na avoid in
-	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
-      (avoid, env, []) names tys in
-  let ntys = Array.length tys in
-  let v = Array.map2
-    (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t))
-    bodies tys in
-  GRec(GCoFix n,Array.of_list (List.rev lfi),
-       Array.map (fun (bl,_,_) -> bl) v,
-       Array.map (fun (_,_,ty) -> ty) v,
-       Array.map (fun (_,bd,_) -> bd) v)
-
-and share_names d flags n l avoid env sigma c t =
-  match EConstr.kind sigma c, EConstr.kind sigma t with
-    (* factorize even when not necessary to have better presentation *)
-    | Lambda (na,t,c), Prod (na',t',c') ->
-        let na = match (na,na') with
-            Name _, _ -> na
-          | _, Name _ -> na'
-          | _ -> na in
-        let t' = detype d flags avoid env sigma t in
-	let id = next_name_away na avoid in
-        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
-        share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
-    (* May occur for fix built interactively *)
-    | LetIn (na,b,t',c), _ when n > 0 ->
-        let t'' = detype d flags avoid env sigma t' in
-        let b' = detype d flags avoid env sigma b in
-	let id = next_name_away na avoid in
-        let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
-        share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
-    (* Only if built with the f/n notation or w/o let-expansion in types *)
-    | _, LetIn (_,b,_,t) when n > 0 ->
-	share_names d flags n l avoid env sigma c (subst1 b t)
-    (* If it is an open proof: we cheat and eta-expand *)
-    | _, Prod (na',t',c') when n > 0 ->
-        let t'' = detype d flags avoid env sigma t' in
-	let id = next_name_away na' avoid in
-        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
-        let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
-    (* If built with the f/n notation: we renounce to share names *)
-    | _ ->
-        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
-        let c = detype d flags avoid env sigma c in
-        let t = detype d flags avoid env sigma t in
-        (List.rev l,c,t)
+    | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef
+    | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef
 
 and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 32b94e1b0..817b8ba6e 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -56,6 +56,13 @@ val detype_sort : evar_map -> Sorts.t -> glob_sort
 val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> 
   evar_map -> rel_context -> 'a glob_decl_g list
 
+val share_pattern_names :
+  (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int ->
+  (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list ->
+  Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern ->
+  Pattern.constr_pattern ->
+  (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a
+
 val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
 
 (** look for the index of a named var or a nondep var as it is renamed *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 74f2cefab..e89bbf7c3 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
   | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) ->
     f m1 m2 && Name.equal pat1 pat2 &&
     Option.equal f p1 p2 && f c1 c2 && f t1 t2
-  | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) ->
+  | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) ->
     fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
     Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
     Array.equal f c1 c2 && Array.equal f t1 t2
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index dcb93bfb6..e52112fda 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -15,7 +15,6 @@ open Globnames
 open Nameops
 open Term
 open Constr
-open Vars
 open Glob_term
 open Pp
 open Mod_subst
@@ -57,10 +56,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   constr_pattern_eq p1 p2 &&
   constr_pattern_eq r1 r2 &&
   List.equal pattern_eq l1 l2
-| PFix f1, PFix f2 ->
-  fixpoint_eq f1 f2
-| PCoFix f1, PCoFix f2 ->
-  cofixpoint_eq f1 f2
+| PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) ->
+  Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq f1 f2
+| PCoFix (i1,f1), PCoFix (i2,f2) ->
+  Int.equal i1 i2 && rec_declaration_eq f1 f2
 | PProj (p1, t1), PProj (p2, t2) ->
    Projection.equal p1 p2 && constr_pattern_eq t1 t2
 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
@@ -71,19 +70,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
   Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2
 
-and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) =
-  Int.equal i1 i2 &&
-  Array.equal Int.equal arg1 arg2 &&
-  rec_declaration_eq r1 r2
-
-and cofixpoint_eq (i1, r1) (i2, r2) =
-  Int.equal i1 i2 &&
-  rec_declaration_eq r1 r2
-
 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
   Array.equal Name.equal n1 n2 &&
-  Array.equal Constr.equal c1 c2 &&
-  Array.equal Constr.equal r1 r2
+  Array.equal constr_pattern_eq c1 c2 &&
+  Array.equal constr_pattern_eq r1 r2
 
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
@@ -123,8 +113,10 @@ let rec occurn_pattern n = function
   | PMeta _ | PSoApp _ -> true
   | PEvar (_,args) -> Array.exists (occurn_pattern n) args
   | PVar _ | PRef _ | PSort _ -> false
-  | PFix fix -> not (noccurn n (mkFix fix))
-  | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+  | PFix (_,(_,tl,bl)) ->
+     Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
+  | PCoFix (_,(_,tl,bl)) ->
+     Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
 
 let noccurn_pattern n c = not (occurn_pattern n c)
 
@@ -209,8 +201,16 @@ let pattern_of_constr env sigma t =
 	in
 	PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
 	       Array.to_list (Array.mapi branch_of_constr br))
-    | Fix f -> PFix f
-    | CoFix f -> PCoFix f in
+    | Fix (lni,(lna,tl,bl)) ->
+       let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+       let env' = Array.fold_left2 push env lna tl in
+       PFix (lni,(lna,Array.map (pattern_of_constr env) tl,
+                  Array.map (pattern_of_constr env') bl))
+    | CoFix (ln,(lna,tl,bl)) ->
+       let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+       let env' = Array.fold_left2 push env lna tl in
+       PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl,
+                  Array.map (pattern_of_constr env') bl)) in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -225,10 +225,14 @@ let map_pattern_with_binders g f l = function
   | PCase (ci,po,p,pl) ->
     PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
   | PProj (p,pc) -> PProj (p, f l pc)
+  | PFix (lni,(lna,tl,bl)) ->
+     let l' = Array.fold_left (fun l na -> g na l) l lna in
+     PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl))
+  | PCoFix (ln,(lna,tl,bl)) ->
+     let l' = Array.fold_left (fun l na -> g na l) l lna in
+     PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
   (* Non recursive *)
-  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _
-  (* Bound to terms *)
-  | PFix _ | PCoFix _ as x) -> x
+  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x
 
 let error_instantiate_pattern id l =
   let is = match l with
@@ -262,15 +266,12 @@ let instantiate_pattern env sigma lvar c =
 	  error_instantiate_pattern id (List.subtract Id.equal ctx vars)
        with Not_found (* Map.find failed *) ->
 	 x)
-  | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.")
   | c ->
       map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
   aux [] c
 
 let rec liftn_pattern k n = function
   | PRel i as x -> if i >= n then PRel (i+k) else x
-  | PFix x -> PFix (destFix (liftn k n (mkFix x)))
-  | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
   | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c
 
 let lift_pattern k = liftn_pattern k 1
@@ -337,19 +338,35 @@ let rec subst_pattern subst pat =
       if cip' == cip && typ' == typ && c' == c && branches' == branches
       then pat
       else PCase(cip', typ', c', branches')
-  | PFix fixpoint ->
-      let cstr = mkFix fixpoint in
-      let fixpoint' = destFix (subst_mps subst cstr) in
-	if fixpoint' == fixpoint then pat else
-	  PFix fixpoint'
-  | PCoFix cofixpoint ->
-      let cstr = mkCoFix cofixpoint in
-      let cofixpoint' = destCoFix (subst_mps subst cstr) in
-	if cofixpoint' == cofixpoint then pat else
-	  PCoFix cofixpoint'
-
-let mkPLambda na b = PLambda(na,PMeta None,b)
-let rev_it_mkPLambda = List.fold_right mkPLambda
+  | PFix (lni,(lna,tl,bl)) ->
+      let tl' = Array.smartmap (subst_pattern subst) tl in
+      let bl' = Array.smartmap (subst_pattern subst) bl in
+      if bl' == bl && tl' == tl then pat
+      else PFix (lni,(lna,tl',bl'))
+  | PCoFix (ln,(lna,tl,bl)) ->
+      let tl' = Array.smartmap (subst_pattern subst) tl in
+      let bl' = Array.smartmap (subst_pattern subst) bl in
+      if bl' == bl && tl' == tl then pat
+      else PCoFix (ln,(lna,tl',bl'))
+
+let mkPLetIn na b t c = PLetIn(na,b,t,c)
+let mkPProd na t u = PProd(na,t,u)
+let mkPLambda na t b = PLambda(na,t,b)
+let mkPLambdaUntyped na b = PLambda(na,PMeta None,b)
+let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped
+
+let mkPProd_or_LetIn (na,_,bo,t) c =
+  match bo with
+  | None -> mkPProd na t c
+  | Some b -> mkPLetIn na b (Some t) c
+
+let mkPLambda_or_LetIn (na,_,bo,t) c =
+  match bo with
+  | None -> mkPLambda na t c
+  | Some b -> mkPLetIn na b (Some t) c
+
+let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c)
+let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c)
 
 let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp
 
@@ -428,7 +445,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       let pred = match p,indnames with
         | Some p, Some {CAst.v=(_,nal)} ->
           let nvars = na :: List.rev nal @ vars in
-          rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
+          rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p))
         | None, _ -> PMeta None
 	| Some p, None ->
           match DAst.get p with
@@ -450,9 +467,40 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
   | GProj(p,c) ->
     PProj(p, pat_of_raw metas vars c)
 
-  | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
+  | GRec (GFix (ln,n), ids, decls, tl, cl) ->
+    if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
+      err ?loc (Pp.str "\"struct\" annotation is expected.")
+    else
+      let ln = Array.map (fst %> Option.get) ln in
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+      let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+      let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+      let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+      let names = Array.map (fun id -> Name id) ids in
+      PFix ((ln,n), (names, tl, cl))
+
+  | GRec (GCoFix n, ids, decls, tl, cl) ->
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+      let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+      let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+      let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+      let names = Array.map (fun id -> Name id) ids in
+      PCoFix (n, (names, tl, cl))
+
+  | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
       err ?loc (Pp.str "Non supported pattern."))
 
+and pat_of_glob_in_context metas vars decls c =
+  let rec aux acc vars = function
+    | (na,bk,b,t) :: decls ->
+       let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in
+       aux (decl::acc) (na::vars) decls
+    | [] ->
+       acc, pat_of_raw metas vars c
+  in aux [] vars decls
+
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg p = match DAst.get p with
     | PatVar na ->
@@ -477,7 +525,7 @@ and pats_of_glob_branches loc metas vars ind brs =
             (str "No unique branch for " ++ int j ++ str"-th constructor.");
         let lna = List.map get_arg lv in
         let vars' = List.rev lna @ vars in
-        let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
+        let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in
         let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
         let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
         ext, ((j-1, tags, pat) :: pats)
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.