Make eq_pattern_test/eq_test work up to the equivalence of primitive

projections with their eta-expanded constant form.

4 files changed, 20 insertions, 18 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index ef94854875..d8698a1651 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 44e435e693..b24c958074 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 8dafadbe49..67aef0cfcd 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 d03fd85211..3f7f238c41 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")