11 files changed, 45 insertions, 13 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 930ab7508..bdc4c067a 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -90,7 +90,8 @@ let rec lookup_named id = function
 let named_context_length = List.length
 let named_context_equal = List.equal eq_named_declaration
 
-let vars_of_named_context = List.map (fun (id,_,_) -> id)
+let vars_of_named_context ctx =
+  List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx
 
 let instance_from_named_context sign =
   let filter = function
diff --git a/kernel/context.mli b/kernel/context.mli
index ad6d645cd..048edef95 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -56,7 +56,7 @@ type rel_context = rel_declaration list
 
 val empty_named_context : named_context
 val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.t list
+val vars_of_named_context : named_context -> Id.Set.t
 
 val lookup_named : Id.t -> named_context -> named_declaration
 
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 0a96821a3..65efb4fd0 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -18,6 +18,9 @@ open Names
  *)
 type level = Expand | Level of int | Opaque
 let default = Level 0
+let is_default = function
+| Level 0 -> true
+| _ -> false
 let transparent = default
 let is_transparent = function
 | Level 0 -> true
@@ -45,11 +48,11 @@ let set_strategy k l =
   match k with
   | VarKey id ->
       var_opacity :=
-      if l=default then Id.Map.remove id !var_opacity
+      if is_default l then Id.Map.remove id !var_opacity
       else Id.Map.add id l !var_opacity
   | ConstKey c ->
       cst_opacity :=
-      if l=default then Cmap.remove c !cst_opacity
+      if is_default l then Cmap.remove c !cst_opacity
       else Cmap.add c l !cst_opacity
   | RelKey _ -> Errors.error "set_strategy: RelKey"
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9b18db78e..ae6817a76 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -228,7 +228,7 @@ let lookup_constructor_variables (ind,_) env =
 
 let vars_of_global env constr =
   match kind_of_term constr with
-      Var id -> [id]
+      Var id -> Id.Set.singleton id
     | Const kn -> lookup_constant_variables kn env
     | Ind ind -> lookup_inductive_variables ind env
     | Construct cstr -> lookup_constructor_variables cstr env
@@ -239,7 +239,7 @@ let global_vars_set env constr =
     let acc =
       match kind_of_term c with
       | Var _ | Const _ | Ind _ | Construct _ ->
-	  List.fold_right Id.Set.add (vars_of_global env c) acc
+	  Id.Set.union (vars_of_global env c) acc
       | _ ->
 	  acc in
     fold_constr filtrec acc c
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 54e88f646..d378501a0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -165,7 +165,7 @@ val set_engagement : engagement -> env -> env
 val global_vars_set : env -> constr -> Id.Set.t
 
 (** the constr must be a global reference *)
-val vars_of_global : env -> constr -> Id.t list
+val vars_of_global : env -> constr -> Id.Set.t
 
 val keep_hyps : env -> Id.Set.t -> section_context
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 4e3da3d8c..cde45a81f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -79,8 +79,18 @@ let we_are_parsing = ref false
    For correct comparisons, this constructor should remain the last one. *)
 
 type compat_version = V8_2 | V8_3 | V8_4 | Current
+
 let compat_version = ref Current
-let version_strictly_greater v = !compat_version > v
+
+let version_strictly_greater v = match !compat_version, v with
+| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false
+| V8_3, (V8_3 | V8_4 | Current) -> false
+| V8_4, (V8_4 | Current) -> false
+| Current, Current -> false
+| V8_3, V8_2 -> true
+| V8_4, (V8_2 | V8_3) -> true
+| Current, (V8_2 | V8_3 | V8_4) -> true
+
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
diff --git a/library/globnames.ml b/library/globnames.ml
index e80197030..af4ebde7f 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -82,7 +82,13 @@ let global_ord_gen ord_cst ord_ind ord_cons x y = match x, y with
   | IndRef indx, IndRef indy -> ord_ind indx indy
   | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
   | VarRef v1, VarRef v2 -> Id.compare v1 v2
-  | _, _ -> Pervasives.compare x y
+
+  | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1
+  | ConstRef _, VarRef _ -> 1
+  | ConstRef _, (IndRef _ | ConstructRef _) -> -1
+  | IndRef _, (VarRef _ | ConstRef _) -> 1
+  | IndRef _, ConstructRef _ -> -1
+  | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1
 
 let global_ord_can =
   global_ord_gen con_ord ind_ord constructor_ord
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 4cb94e38b..0ff94d395 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -19,6 +19,18 @@ type t =
   | LEFTQMARK
   | EOI
 
+let equal t1 t2 = match t1, t2 with
+| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
+| METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2
+| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
+| IDENT s1, IDENT s2 -> CString.equal s1 s2
+| FIELD s1, FIELD s2 -> CString.equal s1 s2
+| INT s1, INT s2 -> CString.equal s1 s2
+| STRING s1, STRING s2 -> CString.equal s1 s2
+| LEFTQMARK, LEFTQMARK -> true
+| EOI, EOI -> true
+| _ -> false
+
 let extract_string = function
   | KEYWORD s -> s
   | IDENT s -> s
@@ -89,4 +101,4 @@ let match_pattern =
     | "EOI", "" -> (function EOI -> "" | _ -> err ())
     | pat ->
 	let tok = of_pattern pat in
-	function tok' -> if tok = tok' then snd pat else err ()
+	function tok' -> if equal tok tok' then snd pat else err ()
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a4fc330c6..fc5fc0d2c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -273,7 +273,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        acc2 := List.fold_right Id.Set.add (vars_of_global (Global.env()) c) !acc2
+        acc2 := Id.Set.union (vars_of_global (Global.env()) c) !acc2
     | _ ->
         iter_constr_with_full_binders
           (fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index de394e660..d2f53e953 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -390,7 +390,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 
       | ( Const _ | Ind _ | Construct _ ) ->
           let vars = Environ.vars_of_global (Global.env()) c in
-            List.iter check vars; c
+            Id.Set.iter check vars; c
 
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 66a656ad7..908010428 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -523,7 +523,7 @@ let occur_evar n c =
 
 let occur_in_global env id constr =
   let vars = vars_of_global env constr in
-  if List.mem id vars then raise Occur
+  if Id.Set.mem id vars then raise Occur
 
 let occur_var env id c =
   let rec occur_rec c =