1 files changed, 50 insertions, 10 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0413c6b6..d7118efd 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -13,6 +13,7 @@ open Pp
 open CErrors
 open Util
 open Names
+open Constr
 open Globnames
 open Termops
 open Term
@@ -20,7 +21,6 @@ open EConstr
 open Vars
 open Pattern
 open Patternops
-open Misctypes
 open Context.Rel.Declaration
 open Ltac_pretype
 (*i*)
@@ -185,9 +185,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
@@ -252,9 +279,10 @@ let matches_core env sigma allow_bound_rels
 
       | PSort ps, Sort s ->
 
+        let open Glob_term in
         begin match ps, ESorts.kind sigma s with
-        | GProp, Prop Null -> subst
-        | GSet, Prop Pos -> subst
+        | GProp, Prop -> subst
+        | GSet, Set -> subst
         | GType _, Type _ -> subst
         | _ -> raise PatternMatchingFailure
         end
@@ -366,8 +394,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 _
@@ -392,7 +432,7 @@ let special_meta = (-1)
 
 type matching_result =
     { m_sub : bound_ident_map * patvar_map;
-      m_ctx : constr; }
+      m_ctx : constr Lazy.t; }
 
 let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
 
@@ -416,7 +456,7 @@ let authorized_occ env sigma closed pat c mk_ctx =
     let subst = matches_core_closed env sigma pat c in
     if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
     then (fun next -> next ())
-    else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
+    else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next)
   with PatternMatchingFailure -> (fun next -> next ())
 
 let subargs env v = Array.map_to_list (fun c -> (env, c)) v