diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 11:09:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 21:05:06 +0200 |
| commit | c955779074833066e9db81c9fb1b32493cfebfa2 (patch) | |
| tree | b5268515c605ea0336b0233e5d751ab57311bc15 /pretyping/find_subterm.ml | |
| parent | 9ec08ac299faf6acdfd6061fd21a00e3446aec79 (diff) | |
Make eq_pattern_test/eq_test work up to the equivalence of primitive
projections with their eta-expanded constant form.
Diffstat (limited to 'pretyping/find_subterm.ml')
| -rw-r--r-- | pretyping/find_subterm.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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 |