Index keys instead of simply global references.

1 files changed, 5 insertions, 21 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1a1143fe7b..efa64ca1ea 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")