Merge PR#379: Introducing evar-insensitive constrs

3 files changed, 8 insertions, 6 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 836568b890..a63264b669 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -228,10 +228,12 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na (_,b as envnames_b) =
+let find_displayed_name_in all avoid na (env, b) =
+  let b = EConstr.of_constr b in
+  let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in flag avoid na b
-  else compute_displayed_name_in flag avoid na b
+  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
+  else compute_displayed_name_in Evd.empty flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
diff --git a/library/keys.ml b/library/keys.ml
index 057dc3b65d..c9e325ee57 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -114,11 +114,11 @@ let inKeys : key_obj -> obj =
 let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
 
-let constr_key c =
+let constr_key kind c =
   let open Globnames in 
   try 
     let rec aux k = 
-      match kind_of_term k with
+      match kind k with
       | Const (c, _) -> KGlob (ConstRef c)
       | Ind (i, u) -> KGlob (IndRef i)
       | Construct (c,u) -> KGlob (ConstructRef c)
diff --git a/library/keys.mli b/library/keys.mli
index 69668590d6..6abac4de44 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -16,7 +16,7 @@ val declare_equiv_keys : key -> key -> unit
 val equiv_keys : key -> key -> bool
 (** Check equivalence of keys. *)
 
-val constr_key : Term.constr -> key option
+val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
 (** Compute the head key of a term. *)
 
 val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds