aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/univ.ml14
-rw-r--r--kernel/constr.ml28
-rw-r--r--kernel/cooking.ml12
-rw-r--r--kernel/names.ml58
-rw-r--r--kernel/names.mli26
-rw-r--r--kernel/sorts.ml2
-rw-r--r--kernel/univ.ml22
-rw-r--r--lib/cSet.ml2
-rw-r--r--lib/hashcons.ml12
-rw-r--r--lib/hashcons.mli12
-rw-r--r--lib/hashset.ml4
-rw-r--r--lib/hashset.mli2
-rw-r--r--pretyping/coercion.ml18
-rw-r--r--printing/printer.ml3
-rw-r--r--proofs/pfedit.ml3
-rw-r--r--stm/lemmas.ml10
-rw-r--r--theories/Classes/CMorphisms.v2
-rw-r--r--tools/coq_makefile.ml34
-rw-r--r--toplevel/record.ml8
19 files changed, 183 insertions, 89 deletions
diff --git a/checker/univ.ml b/checker/univ.ml
index cb2eaced7..96d827013 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -33,7 +33,7 @@ module type Hashconsed =
sig
type t
val hash : t -> int
- val equal : t -> t -> bool
+ val eq : t -> t -> bool
val hcons : t -> t
end
@@ -51,7 +51,7 @@ struct
type t = _t
type u = (M.t -> M.t)
let hash = function Nil -> 0 | Cons (_, h, _) -> h
- let equal l1 l2 = match l1, l2 with
+ let eq l1 l2 = match l1, l2 with
| Nil, Nil -> true
| Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
| _ -> false
@@ -131,7 +131,7 @@ module HList = struct
let rec remove x = function
| Nil -> nil
| Cons (y, _, l) ->
- if H.equal x y then l
+ if H.eq x y then l
else cons y (remove x l)
end
@@ -229,7 +229,7 @@ module Level = struct
type _t = t
type t = _t
type u = unit
- let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+ let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
let hash x = x.hash
let hashcons () x =
let data' = RawLevel.hcons x.data in
@@ -320,7 +320,7 @@ struct
let hashcons hdir (b,n as x) =
let b' = hdir b in
if b' == b then x else (b',n)
- let equal l1 l2 =
+ let eq l1 l2 =
l1 == l2 ||
match l1,l2 with
| (b,n), (b',n') -> b == b' && n == n'
@@ -339,7 +339,7 @@ struct
let hcons =
Hashcons.simple_hcons H.generate H.hcons Level.hcons
let hash = ExprHash.hash
- let equal x y = x == y ||
+ let eq x y = x == y ||
(let (u,n) = x and (v,n') = y in
Int.equal n n' && Level.equal u v)
@@ -1089,7 +1089,7 @@ struct
a
end
- let equal t1 t2 =
+ let eq t1 t2 =
t1 == t2 ||
(Int.equal (Array.length t1) (Array.length t2) &&
let rec aux i =
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8e05e29eb..ce20751ab 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -744,12 +744,10 @@ let hasheq t1 t2 =
n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2
| App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2
| Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2
- | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2
| Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
- | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) ->
- sp1 == sp2 && Int.equal i1 i2 && u1 == u2
- | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) ->
- sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && u1 == u2
+ | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
+ | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
| Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) ->
ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2
| Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
@@ -769,10 +767,10 @@ let hasheq t1 t2 =
once and for all the table we'll use for hash-consing all constr *)
module HashsetTerm =
- Hashset.Make(struct type t = constr let equal = hasheq end)
+ Hashset.Make(struct type t = constr let eq = hasheq end)
module HashsetTermArray =
- Hashset.Make(struct type t = constr array let equal = array_eqeq end)
+ Hashset.Make(struct type t = constr array let eq = array_eqeq end)
let term_table = HashsetTerm.create 19991
(* The associative table to hashcons terms. *)
@@ -827,19 +825,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
| Proj (p,c) ->
let c, hc = sh_rec c in
let p' = Projection.hcons p in
- (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc))
+ (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc))
| Const (c,u) ->
let c' = sh_con c in
let u', hu = sh_instance u in
- (Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu))
- | Ind ((kn,i) as ind,u) ->
+ (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu))
+ | Ind (ind,u) ->
let u', hu = sh_instance u in
(Ind (sh_ind ind, u'),
- combinesmall 10 (combine (ind_hash ind) hu))
- | Construct ((((kn,i),j) as c,u))->
+ combinesmall 10 (combine (ind_syntactic_hash ind) hu))
+ | Construct (c,u) ->
let u', hu = sh_instance u in
(Construct (sh_construct c, u'),
- combinesmall 11 (combine (constructor_hash c) hu))
+ combinesmall 11 (combine (constructor_syntactic_hash c) hu))
| Case (ci,p,c,bl) ->
let p, hp = sh_rec p
and c, hc = sh_rec c in
@@ -942,7 +940,7 @@ struct
List.equal (==) info1.ind_tags info2.ind_tags &&
Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags &&
info1.style == info2.style
- let equal ci ci' =
+ let eq ci ci' =
ci.ci_ind == ci'.ci_ind &&
Int.equal ci.ci_npar ci'.ci_npar &&
Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
@@ -984,7 +982,7 @@ module Hsorts =
let hashcons huniv = function
Prop c -> Prop c
| Type u -> Type (huniv u)
- let equal s1 s2 =
+ let eq s1 s2 =
s1 == s2 ||
match (s1,s2) with
(Prop c1, Prop c2) -> c1 == c2
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 86d786b09..6dc2a617d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -44,15 +44,15 @@ module RefHash =
struct
type t = my_global_reference
let equal gr1 gr2 = match gr1, gr2 with
- | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2
- | IndRef i1, IndRef i2 -> eq_ind i1 i2
- | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2
+ | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
+ | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
+ | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
| _ -> false
open Hashset.Combine
let hash = function
- | ConstRef c -> combinesmall 1 (Constant.hash c)
- | IndRef i -> combinesmall 2 (ind_hash i)
- | ConstructRef c -> combinesmall 3 (constructor_hash c)
+ | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
+ | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
+ | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
end
module RefTable = Hashtbl.Make(RefHash)
diff --git a/kernel/names.ml b/kernel/names.ml
index 0aa26fb9c..8e0237863 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -111,7 +111,7 @@ struct
let hashcons hident = function
| Name id -> Name (hident id)
| n -> n
- let equal n1 n2 =
+ let eq n1 n2 =
n1 == n2 ||
match (n1,n2) with
| (Name id1, Name id2) -> id1 == id2
@@ -245,7 +245,7 @@ struct
type t = _t
type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t)
let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
- let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+ let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
(x == y) ||
(Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
let hash = hash
@@ -341,7 +341,7 @@ module ModPath = struct
| MPfile dir -> MPfile (hdir dir)
| MPbound m -> MPbound (huniqid m)
| MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
- let rec equal d1 d2 =
+ let rec eq d1 d2 =
d1 == d2 ||
match d1,d2 with
| MPfile dir1, MPfile dir2 -> dir1 == dir2
@@ -441,7 +441,7 @@ module KerName = struct
let hashcons (hmod,hdir,hstr) kn =
let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
{ modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
- let equal kn1 kn2 =
+ let eq kn1 kn2 =
kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
kn1.knlabel == kn2.knlabel
let hash = hash
@@ -495,7 +495,7 @@ module KerPair = struct
| Dual (kn,_) -> kn
let same kn = Same kn
- let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
+ let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
let make1 = same
let make2 mp l = same (KerName.make2 mp l)
@@ -542,6 +542,23 @@ module KerPair = struct
let hash x = KerName.hash (canonical x)
end
+ module SyntacticOrd = struct
+ type t = kernel_pair
+ let compare x y = match x, y with
+ | Same knx, Same kny -> KerName.compare knx kny
+ | Dual (knux,kncx), Dual (knuy,kncy) ->
+ let c = KerName.compare knux knuy in
+ if not (Int.equal c 0) then c
+ else KerName.compare kncx kncy
+ | Same _, _ -> -1
+ | Dual _, _ -> 1
+ let equal x y = x == y || compare x y = 0
+ let hash = function
+ | Same kn -> KerName.hash kn
+ | Dual (knu, knc) ->
+ Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
+ end
+
(** Default (logical) comparison and hash is on the canonical part *)
let equal = CanOrd.equal
let hash = CanOrd.hash
@@ -553,7 +570,7 @@ module KerPair = struct
let hashcons hkn = function
| Same kn -> Same (hkn kn)
| Dual (knu,knc) -> make (hkn knu) (hkn knc)
- let equal x y = (* physical comparison on subterms *)
+ let eq x y = (* physical comparison on subterms *)
x == y ||
match x,y with
| Same x, Same y -> x == y
@@ -613,6 +630,8 @@ let index_of_constructor (ind, i) = i
let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2
let eq_user_ind (m1, i1) (m2, i2) =
Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
+let eq_syntactic_ind (m1, i1) (m2, i2) =
+ Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
let ind_ord (m1, i1) (m2, i2) =
let c = Int.compare i1 i2 in
@@ -620,15 +639,22 @@ let ind_ord (m1, i1) (m2, i2) =
let ind_user_ord (m1, i1) (m2, i2) =
let c = Int.compare i1 i2 in
if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
+let ind_syntactic_ord (m1, i1) (m2, i2) =
+ let c = Int.compare i1 i2 in
+ if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
let ind_hash (m, i) =
Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
let ind_user_hash (m, i) =
Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
+let ind_syntactic_hash (m, i) =
+ Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
let eq_user_constructor (ind1, j1) (ind2, j2) =
Int.equal j1 j2 && eq_user_ind ind1 ind2
+let eq_syntactic_constructor (ind1, j1) (ind2, j2) =
+ Int.equal j1 j2 && eq_syntactic_ind ind1 ind2
let constructor_ord (ind1, j1) (ind2, j2) =
let c = Int.compare j1 j2 in
@@ -636,11 +662,16 @@ let constructor_ord (ind1, j1) (ind2, j2) =
let constructor_user_ord (ind1, j1) (ind2, j2) =
let c = Int.compare j1 j2 in
if Int.equal c 0 then ind_user_ord ind1 ind2 else c
+let constructor_syntactic_ord (ind1, j1) (ind2, j2) =
+ let c = Int.compare j1 j2 in
+ if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c
let constructor_hash (ind, i) =
Hashset.Combine.combine (ind_hash ind) (Int.hash i)
let constructor_user_hash (ind, i) =
Hashset.Combine.combine (ind_user_hash ind) (Int.hash i)
+let constructor_syntactic_hash (ind, i) =
+ Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i)
module InductiveOrdered = struct
type t = inductive
@@ -685,7 +716,7 @@ module Hind = Hashcons.Make(
type t = inductive
type u = MutInd.t -> MutInd.t
let hashcons hmind (mind, i) = (hmind mind, i)
- let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
+ let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
let hash = ind_hash
end)
@@ -694,7 +725,7 @@ module Hconstruct = Hashcons.Make(
type t = constructor
type u = inductive -> inductive
let hashcons hind (ind, j) = (hind ind, j)
- let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
+ let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
let hash = constructor_hash
end)
@@ -828,13 +859,22 @@ struct
let hash (c, b) = (if b then 0 else 1) + Constant.hash c
+ module SyntacticOrd = struct
+ type t = constant * bool
+ let compare (c, b) (c', b') =
+ if b = b' then Constant.SyntacticOrd.compare c c' else -1
+ let equal (c, b as x) (c', b' as x') =
+ x == x' || b = b' && Constant.SyntacticOrd.equal c c'
+ let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c
+ end
+
module Self_Hashcons =
struct
type _t = t
type t = _t
type u = Constant.t -> Constant.t
let hashcons hc (c,b) = (hc c,b)
- let equal ((c,b) as x) ((c',b') as y) =
+ let eq ((c,b) as x) ((c',b') as y) =
x == y || (c == c' && b == b')
let hash = hash
end
diff --git a/kernel/names.mli b/kernel/names.mli
index 6380b17fb..1dfdd8290 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -325,6 +325,12 @@ sig
val hash : t -> int
end
+ module SyntacticOrd : sig
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
val equal : t -> t -> bool
(** Default comparison, alias for [CanOrd.equal] *)
@@ -399,6 +405,12 @@ sig
val hash : t -> int
end
+ module SyntacticOrd : sig
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
val equal : t -> t -> bool
(** Default comparison, alias for [CanOrd.equal] *)
@@ -442,16 +454,22 @@ val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
val eq_ind : inductive -> inductive -> bool
val eq_user_ind : inductive -> inductive -> bool
+val eq_syntactic_ind : inductive -> inductive -> bool
val ind_ord : inductive -> inductive -> int
val ind_hash : inductive -> int
val ind_user_ord : inductive -> inductive -> int
val ind_user_hash : inductive -> int
+val ind_syntactic_ord : inductive -> inductive -> int
+val ind_syntactic_hash : inductive -> int
val eq_constructor : constructor -> constructor -> bool
val eq_user_constructor : constructor -> constructor -> bool
+val eq_syntactic_constructor : constructor -> constructor -> bool
val constructor_ord : constructor -> constructor -> int
-val constructor_user_ord : constructor -> constructor -> int
val constructor_hash : constructor -> int
+val constructor_user_ord : constructor -> constructor -> int
val constructor_user_hash : constructor -> int
+val constructor_syntactic_ord : constructor -> constructor -> int
+val constructor_syntactic_hash : constructor -> int
(** Better to have it here that in Closure, since required in grammar.cma *)
type evaluable_global_reference =
@@ -665,6 +683,12 @@ module Projection : sig
val make : constant -> bool -> t
+ module SyntacticOrd : sig
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
val constant : t -> constant
val unfolded : t -> bool
val unfold : t -> t
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index a90736884..62013b38f 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -98,7 +98,7 @@ module Hsorts =
let u' = huniv u in
if u' == u then c else Type u'
| s -> s
- let equal s1 s2 = match (s1,s2) with
+ let eq s1 s2 = match (s1,s2) with
| (Prop c1, Prop c2) -> c1 == c2
| (Type u1, Type u2) -> u1 == u2
|_ -> false
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9d62c9af5..126f95f1f 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -35,7 +35,7 @@ module type Hashconsed =
sig
type t
val hash : t -> int
- val equal : t -> t -> bool
+ val eq : t -> t -> bool
val hcons : t -> t
end
@@ -53,7 +53,7 @@ struct
type t = _t
type u = (M.t -> M.t)
let hash = function Nil -> 0 | Cons (_, h, _) -> h
- let equal l1 l2 = match l1, l2 with
+ let eq l1 l2 = match l1, l2 with
| Nil, Nil -> true
| Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
| _ -> false
@@ -135,12 +135,12 @@ module HList = struct
let rec remove x = function
| Nil -> nil
| Cons (y, _, l) ->
- if H.equal x y then l
+ if H.eq x y then l
else cons y (remove x l)
let rec mem x = function
| Nil -> false
- | Cons (y, _, l) -> H.equal x y || mem x l
+ | Cons (y, _, l) -> H.eq x y || mem x l
let rec compare cmp l1 l2 = match l1, l2 with
| Nil, Nil -> 0
@@ -251,7 +251,7 @@ module Level = struct
type _t = t
type t = _t
type u = unit
- let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+ let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
let hash x = x.hash
let hashcons () x =
let data' = RawLevel.hcons x.data in
@@ -400,7 +400,7 @@ struct
let hashcons hdir (b,n as x) =
let b' = hdir b in
if b' == b then x else (b',n)
- let equal l1 l2 =
+ let eq l1 l2 =
l1 == l2 ||
match l1,l2 with
| (b,n), (b',n') -> b == b' && n == n'
@@ -419,7 +419,7 @@ struct
let hcons =
Hashcons.simple_hcons H.generate H.hcons Level.hcons
let hash = ExprHash.hash
- let equal x y = x == y ||
+ let eq x y = x == y ||
(let (u,n) = x and (v,n') = y in
Int.equal n n' && Level.equal u v)
@@ -724,7 +724,7 @@ module Hconstraint =
type t = univ_constraint
type u = universe_level -> universe_level
let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
- let equal (l1,k,l2) (l1',k',l2') =
+ let eq (l1,k,l2) (l1',k',l2') =
l1 == l1' && k == k' && l2 == l2'
let hash = Hashtbl.hash
end)
@@ -736,7 +736,7 @@ module Hconstraints =
type u = univ_constraint -> univ_constraint
let hashcons huc s =
Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
- let equal s s' =
+ let eq s s' =
List.for_all2eq (==)
(Constraint.elements s)
(Constraint.elements s')
@@ -901,7 +901,7 @@ struct
a
end
- let equal t1 t2 =
+ let eq t1 t2 =
t1 == t2 ||
(Int.equal (Array.length t1) (Array.length t2) &&
let rec aux i =
@@ -1235,7 +1235,7 @@ module Huniverse_set =
type u = universe_level -> universe_level
let hashcons huc s =
LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty
- let equal s s' =
+ let eq s s' =
LSet.equal s s'
let hash = Hashtbl.hash
end)
diff --git a/lib/cSet.ml b/lib/cSet.ml
index 3eeff29fe..037cdc356 100644
--- a/lib/cSet.ml
+++ b/lib/cSet.ml
@@ -57,7 +57,7 @@ struct
open Hashset.Combine
type t = set
type u = M.t -> M.t
- let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
+ let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0
let hashcons = umap
end
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index b5192dbb8..4eaacf914 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -15,7 +15,7 @@
* of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
* [hashcons u x] is a function that hash-cons the sub-structures of x using
* the hash-consing functions u provides.
- * [equal] is a comparison function. It is allowed to use physical equality
+ * [eq] is a comparison function. It is allowed to use physical equality
* on the sub-terms hash-consed by the hashcons function.
* [hash] is the hash function given to the Hashtbl.Make function
*
@@ -27,7 +27,7 @@ module type HashconsedType =
type t
type u
val hashcons : u -> t -> t
- val equal : t -> t -> bool
+ val eq : t -> t -> bool
val hash : t -> int
end
@@ -53,7 +53,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
(* We create the type of hashtables for t, with our comparison fun.
* An invariant is that the table never contains two entries equals
- * w.r.t (=), although the equality on keys is X.equal. This is
+ * w.r.t (=), although the equality on keys is X.eq. This is
* granted since we hcons the subterms before looking up in the table.
*)
module Htbl = Hashset.Make(X)
@@ -110,7 +110,7 @@ module Hlist (D:HashedType) =
let hashcons (hrec,hdata) = function
| x :: l -> hdata x :: hrec l
| l -> l
- let equal l1 l2 =
+ let eq l1 l2 =
l1 == l2 ||
match l1, l2 with
| [], [] -> true
@@ -130,7 +130,7 @@ module Hstring = Make(
type t = string
type u = unit
let hashcons () s =(* incr accesstr;*) s
- external equal : string -> string -> bool = "caml_string_equal" "noalloc"
+ external eq : string -> string -> bool = "caml_string_equal" "noalloc"
(** Copy from CString *)
let rec hash len s i accu =
if i = len then accu
@@ -177,6 +177,6 @@ module Hobj = Make(
type t = Obj.t
type u = (Obj.t -> Obj.t) * unit
let hashcons (hrec,_) = hash_obj hrec
- let equal = comp_obj
+ let eq = comp_obj
let hash = Hashtbl.hash
end)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 04754ba1d..150899cef 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -14,9 +14,9 @@ module type HashconsedType =
sig
(** {6 Generic hashconsing signature}
- Given an equivalence relation [equal], a hashconsing function is a
+ Given an equivalence relation [eq], a hashconsing function is a
function that associates the same canonical element to two elements
- related by [equal]. Usually, the element chosen is canonical w.r.t.
+ related by [eq]. Usually, the element chosen is canonical w.r.t.
physical equality [(==)], so as to reduce memory consumption and
enhance efficiency of equality tests.
@@ -32,15 +32,15 @@ module type HashconsedType =
Usually a tuple of functions. *)
val hashcons : u -> t -> t
(** The actual hashconsing function, using its fist argument to recursively
- hashcons substructures. It should be compatible with [equal], that is
- [equal x (hashcons f x) = true]. *)
- val equal : t -> t -> bool
+ hashcons substructures. It should be compatible with [eq], that is
+ [eq x (hashcons f x) = true]. *)
+ val eq : t -> t -> bool
(** A comparison function. It is allowed to use physical equality
on the sub-terms hashconsed by the [hashcons] function, but it should be
insensible to shallow copy of the compared object. *)
val hash : t -> int
(** A hash function passed to the underlying hashtable structure. [hash]
- should be compatible with [equal], i.e. if [equal x y = true] then
+ should be compatible with [eq], i.e. if [eq x y = true] then
[hash x = hash y]. *)
end
diff --git a/lib/hashset.ml b/lib/hashset.ml
index b2795c6b1..af33544dc 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -16,7 +16,7 @@
module type EqType = sig
type t
- val equal : t -> t -> bool
+ val eq : t -> t -> bool
end
type statistics = {
@@ -183,7 +183,7 @@ module Make (E : EqType) =
if i >= sz then ifnotfound index
else if h = hashes.(i) then begin
match Weak.get bucket i with
- | Some v when E.equal v d -> v
+ | Some v when E.eq v d -> v
| _ -> loop (i + 1)
end else loop (i + 1)
in
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 05d4fe379..733c89621 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -16,7 +16,7 @@
module type EqType = sig
type t
- val equal : t -> t -> bool
+ val eq : t -> t -> bool
end
type statistics = {
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9d0f391e4..5c7adf1aa 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -129,7 +129,7 @@ let mu env evdref t =
let rec aux v =
let v' = hnf env !evdref v in
match disc_subset v' with
- Some (u, p) ->
+ | Some (u, p) ->
let f, ct = aux u in
let p = hnf_nodelta env !evdref p in
(Some (fun x ->
@@ -243,7 +243,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let remove_head a c =
match kind_of_term c with
| Lambda (n, t, t') -> c, t'
- (*| Prod (n, t, t') -> t'*)
| Evar (k, args) ->
let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
evdref := evs;
@@ -299,9 +298,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
with NoSubtacCoercion ->
let typ = Typing.unsafe_type_of env evm c in
let typ' = Typing.unsafe_type_of env evm c' in
- (* if not (is_arity env evm typ) then *)
coerce_application typ typ' c c' l l')
- (* else subco () *)
else
subco ()
| x, y when Constr.equal c c' ->
@@ -309,9 +306,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let evm = !evdref in
let lam_type = Typing.unsafe_type_of env evm c in
let lam_type' = Typing.unsafe_type_of env evm c' in
- (* if not (is_arity env evm lam_type) then ( *)
coerce_application lam_type lam_type' c c' l l'
- (* ) else subco () *)
else subco ()
| _ -> subco ())
| _, _ -> subco ()
@@ -337,10 +332,17 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
raise NoSubtacCoercion
in coerce_unify env x y
+let app_coercion env evdref coercion v =
+ match coercion with
+ | None -> v
+ | Some f ->
+ let v' = Typing.e_solve_evars env evdref (f v) in
+ whd_betaiota !evdref v'
+
let coerce_itf loc env evd v t c1 =
let evdref = ref evd in
let coercion = coerce loc env evdref t c1 in
- let t = Option.map (app_opt env evdref coercion) v in
+ let t = Option.map (app_coercion env evdref coercion) v in
!evdref, t
let saturate_evd env evd =
@@ -426,7 +428,7 @@ let inh_coerce_to_base loc env evd j =
let evdref = ref evd in
let ct, typ' = mu env evdref j.uj_type in
let res =
- { uj_val = app_opt env evdref ct j.uj_val;
+ { uj_val = app_coercion env evdref ct j.uj_val;
uj_type = typ' }
in !evdref, res
else (evd, j)
diff --git a/printing/printer.ml b/printing/printer.ml
index 2e67fa5ff..70b5ffcc4 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -30,7 +30,8 @@ let delayed_emacs_cmd s =
let get_current_context () =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e ->
- (Evd.empty, Global.env())
+ let env = Global.env () in
+ (Evd.from_env env, env)
(**********************************************************************)
(** Terms *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 608ee2c70..5367a907e 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -85,7 +85,8 @@ let get_current_goal_context () =
with NoSuchGoal ->
(* spiwack: returning empty evar_map, since if there is no goal, under focus,
there is no accessible evar either *)
- (Evd.empty, Global.env ())
+ let env = Global.env () in
+ (Evd.from_env env, env)
let current_proof_statement () =
match Proof_global.V82.get_current_initial_conclusions () with
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index ac54028eb..80b3fef19 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -522,5 +522,11 @@ let save_proof ?proof = function
let get_current_context () =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e ->
- let env = Global.env () in
- (Evd.from_env env, env)
+ try (* No more focused goals ? *)
+ let p = Pfedit.get_pftreestate () in
+ let evd = Proof.in_proof p (fun x -> x) in
+ (evd, Global.env ())
+ with Proof_global.NoCurrentProof ->
+ let env = Global.env () in
+ (Evd.from_env env, env)
+
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 627a1a495..1cfca4169 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive
Section Normalize.
Context (A : Type).
- Class Normalizes (m : crelation A) (m' : crelation A) : Prop :=
+ Class Normalizes (m : crelation A) (m' : crelation A) :=
normalizes : relation_equivalence m m'.
(** Current strategy: add [flip] everywhere and reduce using [subrelation]
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index f1ad2c262..7b76514e4 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -43,6 +43,16 @@ let section s =
print_com (String.make (l+2) '#');
print "\n"
+(* These are the Coq library directories that are used for
+ * plugin development
+ *)
+let lib_dirs =
+ ["kernel"; "lib"; "library"; "parsing";
+ "pretyping"; "interp"; "printing"; "intf";
+ "proofs"; "tactics"; "tools"; "toplevel";
+ "stm"; "grammar"; "config"; "ltac"; "engine"]
+
+
let usage () =
output_string stderr "Usage summary:
@@ -452,12 +462,8 @@ let variables is_install opt (args,defs) =
end;
(* Caml executables and relative variables *)
if !some_ml4file || !some_mlfile || !some_mlifile then begin
- print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\
- -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)engine\" -I \"$(COQLIB)pretyping\" \\
- -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\
- -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\
- -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)ltac\" -I \"$(COQLIB)stm\" \\
- -I \"$(COQLIB)grammar\" -I \"$(COQLIB)config\"";
+ print "COQSRCLIBS?=" ;
+ List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ;
List.iter (fun c -> print " \\
-I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
@@ -800,6 +806,21 @@ let check_overlapping_include (_,inc_i,inc_r) =
Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
in aux (inc_i@inc_r)
+(* Generate a .merlin file that references the standard library and
+ * any -I included paths.
+ *)
+let merlin targets (ml_inc,_,_) =
+ print ".merlin:\n";
+ print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+ List.iter (fun c ->
+ printf "\t@echo \"B $(COQLIB) %s\" >> .merlin\n" c)
+ lib_dirs ;
+ List.iter (fun (_,c) ->
+ printf "\t@echo \"B %s\" >> .merlin\n" c;
+ printf "\t@echo \"S %s\" >> .merlin\n" c)
+ ml_inc;
+ print "\n"
+
let do_makefile args =
let has_file var = function
|[] -> var := false
@@ -842,6 +863,7 @@ let do_makefile args =
section "Special targets.";
standard opt;
install targets inc is_install;
+ merlin targets inc;
clean sds sps;
make_makefile sds;
implicit ();
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 96cafb072..93429da5a 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -140,8 +140,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
let _, univ = compute_constructor_level evars env_ar newfs in
let ctx, aritysort = Reduction.dest_arity env0 arity in
assert(List.is_empty ctx); (* Ensured by above analysis *)
- if Sorts.is_prop aritysort ||
- (Sorts.is_set aritysort && is_impredicative_set env0) then
+ if not def && (Sorts.is_prop aritysort ||
+ (Sorts.is_set aritysort && is_impredicative_set env0)) then
arity, evars
else
let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
@@ -419,9 +419,9 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
match fields with
| [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
let class_body = it_mkLambda_or_LetIn field params in
- let _class_type = it_mkProd_or_LetIn arity params in
+ let class_type = it_mkProd_or_LetIn arity params in
let class_entry =
- Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
+ Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 18:12:04 +0000