Merge PR#379: Introducing evar-insensitive constrs

1 files changed, 10 insertions, 6 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a543f1957..9986f439af 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -120,7 +120,7 @@ let lookup_named = lookup_named
 let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map)
 
 let eq_named_context_val c1 c2 =
-   c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2)
+   c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2)
 
 (* A local const is evaluable if it is defined  *)
 
@@ -469,9 +469,11 @@ let lookup_modtype mp env =
 
 (*s Judgments. *)
 
-type unsafe_judgment = {
-  uj_val : constr;
-  uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+  uj_val : 'constr;
+  uj_type : 'types }
+
+type unsafe_judgment = (constr, types) punsafe_judgment
 
 let make_judge v tj =
   { uj_val = v;
@@ -480,10 +482,12 @@ let make_judge v tj =
 let j_val j = j.uj_val
 let j_type j = j.uj_type
 
-type unsafe_type_judgment = {
-  utj_val : constr;
+type 'types punsafe_type_judgment = {
+  utj_val : 'types;
   utj_type : sorts }
 
+type unsafe_type_judgment = types punsafe_type_judgment
+
 (*s Compilation of global declaration *)
 
 let compile_constant_body = Cbytegen.compile_constant_body false