Make eq_pattern_test/eq_test work up to the equivalence of primitive

projections with their eta-expanded constant form.

7 files changed, 62 insertions, 22 deletions

diff --git a/library/universes.ml b/library/universes.ml
index 232573d5f..7fe4258c2 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -215,6 +215,39 @@ let leq_constr_universes m n =
     let res = compare_leq m n in
       res, !cstrs
 
+let compare_head_gen_proj env equ eqs eqc' m n =
+  match kind_of_term m, kind_of_term n with
+  | Proj (p, c), App (f, args)
+  | App (f, args), Proj (p, c) -> 
+    (match kind_of_term f with
+    | Const (p', u) when eq_constant p p' -> 
+      let pb = Environ.lookup_projection p env in
+      let npars = pb.Declarations.proj_npars in
+	if Array.length args == npars + 1 then
+	  eqc' c args.(npars)
+	else false
+    | _ -> false)
+  | _ -> Constr.compare_head_gen equ eqs eqc' m n
+    
+let eq_constr_universes_proj env m n =
+  if m == n then true, Constraints.empty
+  else 
+    let cstrs = ref Constraints.empty in
+    let eq_universes strict l l' = 
+      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+    let eq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else
+	(cstrs := Constraints.add 
+	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
+	 true)
+    in
+    let rec eq_constr' m n = 
+      m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
+    in
+    let res = eq_constr' m n in
+      res, !cstrs
+
 (* Generator of levels *)
 let new_univ_level, set_remote_new_univ_level =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
diff --git a/library/universes.mli b/library/universes.mli
index 6cfee48d2..e4bb21833 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -80,6 +80,10 @@ val eq_constr_universes : constr -> constr -> bool universe_constrained
     alpha, casts, application grouping and the universe constraints in [c]. *)
 val leq_constr_universes : constr -> constr -> bool universe_constrained
 
+(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
+    application grouping and the universe constraints in [c]. *)
+val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
+
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index ef9485487..d8698a165 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -139,9 +139,9 @@ let replace_term_occ_decl_modulo (plocs,hyploc) test bywhat d =
 
 (** Finding an exact subterm *)
 
-let make_eq_univs_test evd c =
+let make_eq_univs_test env evd c =
   { match_fun = (fun evd c' ->
-    let b, cst = Universes.eq_constr_universes c c' in
+    let b, cst = Universes.eq_constr_universes_proj env c c' in
       if b then
 	try Evd.add_universe_constraints evd cst
 	with Evd.UniversesDiffer -> raise (NotUnifiable None)
@@ -151,14 +151,14 @@ let make_eq_univs_test evd c =
   last_found = None
 } 
 
-let subst_closed_term_occ evd occs c t =
-  let test = make_eq_univs_test evd c in
+let subst_closed_term_occ env evd occs c t =
+  let test = make_eq_univs_test env evd c in
   let bywhat () = mkRel 1 in
   let t' = replace_term_occ_modulo occs test bywhat t in
     t', test.testing_state
 
-let subst_closed_term_occ_decl evd (plocs,hyploc) c d =
-  let test = make_eq_univs_test evd c in
+let subst_closed_term_occ_decl env evd (plocs,hyploc) c d =
+  let test = make_eq_univs_test env evd c in
   let bywhat () = mkRel 1 in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 44e435e69..b24c95807 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -12,6 +12,7 @@ open Context
 open Term
 open Evd
 open Pretype_errors
+open Environ
 
 (** Finding subterms, possibly up to some unification function,
     possibly at some given occurrences *)
@@ -34,7 +35,7 @@ type 'a testing_function = {
 
 (** This is the basic testing function, looking for exact matches of a
     closed term *)
-val make_eq_univs_test : evar_map -> constr -> evar_map testing_function
+val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
 
 (** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm
     modulo a testing function [test] and replaces successfully
@@ -53,12 +54,12 @@ val replace_term_occ_decl_modulo :
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
     unifying universes which results in a set of constraints. *)
-val subst_closed_term_occ : evar_map -> occurrences -> constr -> 
+val subst_closed_term_occ : env -> evar_map -> occurrences -> constr -> 
   constr -> constr * evar_map
 
 (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of 
     closed [c] at positions [occl] by [Rel 1] in [decl]. *)
-val subst_closed_term_occ_decl : evar_map ->
+val subst_closed_term_occ_decl : env -> evar_map ->
   occurrences * hyp_location_flag ->
   constr -> named_declaration -> named_declaration * evar_map
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8dafadbe4..67aef0cfc 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1137,7 +1137,7 @@ let abstract_scheme env sigma (locc,a) c =
   if occur_meta a then
     mkLambda (na,ta,c)
   else
-    let c', sigma' = subst_closed_term_occ sigma locc a c in
+    let c', sigma' = subst_closed_term_occ env sigma locc a c in
       mkLambda (na,ta,c') 
 
 let pattern_occs loccs_trm env sigma c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d03fd8521..3f7f238c4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -61,7 +61,7 @@ let abstract_scheme env evd c l lname_typ =
        else *) 
        if occur_meta a then mkLambda_name env (na,ta,t), evd
        else
-	 let t', evd' = Find_subterm.subst_closed_term_occ evd locc a t in
+	 let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in
 	   mkLambda_name env (na,ta,t'), evd')
     (c,evd)
     (List.rev l)
@@ -399,7 +399,8 @@ let key_of env b flags f =
   if subterm_restriction b flags then None else
   match kind_of_term f with
   | Const (cst, u) when is_transparent env (ConstKey cst) &&
-      Cpred.mem cst (snd flags.modulo_delta) ->
+      (Cpred.mem cst (snd flags.modulo_delta)
+       || Environ.is_projection cst env) ->
       Some (IsKey (ConstKey (cst, u)))
   | Var id when is_transparent env (VarKey id) && 
       Id.Pred.mem id (fst flags.modulo_delta) ->
@@ -676,7 +677,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 		    let ty1 = get_type_of curenv ~lax:true sigma c1 in
 		    let ty2 = get_type_of curenv ~lax:true sigma c2 in
 		      unify_0_with_initial_metas substn true env cv_pb 
-			{ flags with modulo_delta = full_transparent_state;
+			{ flags with modulo_conv_on_closed_terms = Some full_transparent_state;
+			  modulo_delta = full_transparent_state;
 			  modulo_betaiota = true }
 			ty1 ty2
 		  with RetypeError _ -> substn
@@ -1344,11 +1346,11 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) =
      Evd.evar_universe_context univs,
      subst_univs_constr subst (nf_evar sigma c))
 
-let make_eq_test evd c =
+let make_eq_test env evd c =
   let out cstr =
     Evd.evar_universe_context cstr.testing_state, c
   in
-    (make_eq_univs_test evd c, out)
+    (make_eq_univs_test env evd c, out)
 
 let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl =
   let id =
@@ -1425,7 +1427,7 @@ let make_abstraction env evd ccl abs =
         (make_pattern_test flags env evd c) c None occs check_occs env ccl
   | AbstractExact (name,c,ty,occs,check_occs) ->
       make_abstraction_core name
-        (make_eq_test evd c) (evd,c) ty occs check_occs env ccl
+        (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl
 
 (* Tries to find an instance of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] until it finds a match.
@@ -1435,8 +1437,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
   let rec matchrec cl =
     let cl = strip_outer_cast cl in
     (try
-       if closed0 cl && not (isEvar cl)
-       then
+       if closed0 cl && not (isEvar cl) then
 	 (try w_typed_unify env evd CONV flags op cl,cl
 	  with ex when Pretype_errors.unsatisfiable_exception ex ->
 	    bestexn := Some ex; error "Unsat")
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 08cf95432..841116a0b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2204,17 +2204,18 @@ let generalized_name c t ids cl = function
    [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai]
    but only those at [occs] in [T] *)
 
-let generalize_goal_gen ids i ((occs,c,b),na) t (cl,evd) =
+let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) =
   let decls,cl = decompose_prod_n_assum i cl in
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in
-  let cl',evd' = subst_closed_term_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in
+  let cl',evd' = subst_closed_term_occ env evd occs c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name c t ids cl' na in
     mkProd_or_LetIn (na,b,t) cl', evd'
 
 let generalize_goal gl i ((occs,c,b),na as o) cl =
   let t = pf_type_of gl c in
-    generalize_goal_gen (pf_ids_of_hyps gl) i o t cl
+  let env = pf_env gl in
+    generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl
 
 let generalize_dep ?(with_let=false) c gl =
   let env = pf_env gl in
@@ -2275,7 +2276,7 @@ let new_generalize_gen_let lconstr =
 	(fun i ((_,c,b),_ as o) (cl, args) ->
 	  let t = Tacmach.New.pf_type_of gl c in
 	  let args = if Option.is_empty b then c :: args else args in
-	    generalize_goal_gen ids i o t cl, args)
+	    generalize_goal_gen env ids i o t cl, args)
 	0 lconstr ((concl, sigma), [])
     in
       Proofview.V82.tclEVARS sigma <*>