diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 14:20:42 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 15:26:51 +0100 |
commit | 96f8d358c7d3c9a08ff2006f42716bc64937dad2 (patch) | |
tree | c7a6503e6b39681aee60e556827614b5b3512778 | |
parent | 49a764bd81ac1b21130d54a1808ce95b9992a36d (diff) |
Fixing pervasive equalities. In particular, I removed the code that deleted
duplicates in kernel side effects. They were chosen according to an equality
that was quite irrelevant, and as expected this patch did not break the
test-suite.
-rw-r--r-- | kernel/declareops.ml | 2 | ||||
-rw-r--r-- | kernel/retroknowledge.ml | 10 | ||||
-rw-r--r-- | tactics/elim.ml | 2 |
3 files changed, 10 insertions, 4 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 7c852a755..1b67de0ea 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -248,7 +248,7 @@ type side_effects = side_effect list let no_seff = ([] : side_effects) let iter_side_effects f l = List.iter f (List.rev l) let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = List.uniquize l +let uniquize_side_effects l = l (** FIXME: there is something dubious here *) let union_side_effects l1 l2 = l1 @ l2 let flatten_side_effects l = List.flatten l let side_effects_of_list l = l diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 4dc01f890..0c03e3299 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -100,8 +100,14 @@ type proactive = entry Proactive.t a finite type describing the fields to the field of proactive retroknowledge (and then to make as many functions as needed in environ.ml) *) -module Reactive = - Map.Make (struct type t = entry let compare = compare end) +module EntryOrd = +struct + type t = entry + let make (e : entry) : constr = Obj.magic e (** WARNING: maybe to be updated. *) + let compare c1 c2 = Constr.compare (make c1) (make c2) +end + +module Reactive = Map.Make (EntryOrd) type reactive_end = {(*information required by the compiler of the VM *) vm_compiling : diff --git a/tactics/elim.ml b/tactics/elim.ml index 81fab6e2b..06f84ecd1 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -107,7 +107,7 @@ let head_in indl t gl = if !up_to_delta then find_mrectype env sigma t else extract_mrectype t - in List.mem ity indl + in List.exists (fun i -> eq_ind i ity) indl with Not_found -> false let decompose_these c l = |