diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 26 |
1 files changed, 5 insertions, 21 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 1a1143fe7..efa64ca1e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1457,38 +1457,22 @@ let make_abstraction env evd ccl abs = make_abstraction_core name (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl -let rec constr_key c = - let open Globnames in - match kind_of_term c with - | Const (c, _) -> ConstRef c - | Ind (i, u) -> IndRef i - | Construct (c,u) -> ConstructRef c - | Var id -> VarRef id - | App (f, _) -> constr_key f - | Proj (p, _) -> ConstRef p - | Cast (p, _, _) -> constr_key p - | Lambda _ - | Prod _ - | Case _ - | Fix _ | CoFix _ - | Rel _ | Meta _ | Evar _ | Sort _ | LetIn _ -> raise Not_found - -let keyed_unify env evd op cl = +let keyed_unify env evd kop cl = if not !keyed_unification then true else - let k1 = constr_key op in - let k2 = constr_key cl in - Globnames.eq_gr k1 k2 || Keys.equiv_keys k1 k2 + let k2 = Keys.constr_key cl in + Keys.equiv_keys kop k2 (* Tries to find an instance of term [cl] in term [op]. Unifies [cl] to every subterm of [op] until it finds a match. Fails if no match is found *) let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let bestexn = ref None in + let kop = Keys.constr_key op in let rec matchrec cl = let cl = strip_outer_cast cl in (try - if closed0 cl && not (isEvar cl) && keyed_unify env evd op cl then + if closed0 cl && not (isEvar cl) && keyed_unify env evd kop 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") |