aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/univ.ml14
-rw-r--r--ide/project_file.ml41
-rw-r--r--kernel/constr.ml28
-rw-r--r--kernel/cooking.ml12
-rw-r--r--kernel/environ.ml2
-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/evarconv.ml73
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/reductionops.mli3
-rw-r--r--proofs/pfedit.ml4
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--tactics/elimschemes.ml20
-rw-r--r--tactics/eqschemes.ml18
-rw-r--r--test-suite/success/apply.v2
-rw-r--r--theories/Init/Notations.v3
-rw-r--r--theories/Init/Specif.v2
-rw-r--r--toplevel/auto_ind_decl.ml42
-rw-r--r--toplevel/ind_tables.ml32
-rw-r--r--toplevel/ind_tables.mli15
27 files changed, 169 insertions, 248 deletions
diff --git a/checker/univ.ml b/checker/univ.ml
index 912d20e0d..3bcb3bc95 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -33,7 +33,7 @@ module type Hashconsed =
sig
type t
val hash : t -> int
- val eq : t -> t -> bool
+ val equal : 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 eq l1 l2 = match l1, l2 with
+ let equal 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.eq x y then l
+ if H.equal 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 eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+ let equal 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
@@ -319,7 +319,7 @@ struct
let hashcons hdir (b,n as x) =
let b' = hdir b in
if b' == b then x else (b',n)
- let eq l1 l2 =
+ let equal l1 l2 =
l1 == l2 ||
match l1,l2 with
| (b,n), (b',n') -> b == b' && n == n'
@@ -338,7 +338,7 @@ struct
let hcons =
Hashcons.simple_hcons H.generate H.hcons Level.hcons
let hash = ExprHash.hash
- let eq x y = x == y ||
+ let equal x y = x == y ||
(let (u,n) = x and (v,n') = y in
Int.equal n n' && Level.equal u v)
@@ -1079,7 +1079,7 @@ struct
a
end
- let eq t1 t2 =
+ let equal t1 t2 =
t1 == t2 ||
(Int.equal (Array.length t1) (Array.length t2) &&
let rec aux i =
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 152f76cc0..f7279f9cf 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -28,7 +28,6 @@ let rec parse_string = parser
and parse_string2 = parser
| [< ''"' >] -> ""
| [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
- | [< >] -> raise Parsing_error
and parse_skip_comment = parser
| [< ''\n'; s >] -> s
| [< 'c; s >] -> parse_skip_comment s
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 644f866b3..e2b1d3fd9 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -732,10 +732,12 @@ 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) -> e1 == e2 && array_eqeq l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2
| Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
- | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
- | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && 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
| 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)) ->
@@ -755,10 +757,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 eq = hasheq end)
+ Hashset.Make(struct type t = constr let equal = hasheq end)
module HashsetTermArray =
- Hashset.Make(struct type t = constr array let eq = array_eqeq end)
+ Hashset.Make(struct type t = constr array let equal = array_eqeq end)
let term_table = HashsetTerm.create 19991
(* The associative table to hashcons terms. *)
@@ -813,19 +815,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.SyntacticOrd.hash p') hc))
+ (Proj (p', c), combinesmall 17 (combine (Projection.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.SyntacticOrd.hash c) hu))
- | Ind (ind,u) ->
+ (Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu))
+ | Ind ((kn,i) as ind,u) ->
let u', hu = sh_instance u in
(Ind (sh_ind ind, u'),
- combinesmall 10 (combine (ind_syntactic_hash ind) hu))
- | Construct (c,u) ->
+ combinesmall 10 (combine (ind_hash ind) hu))
+ | Construct ((((kn,i),j) as c,u))->
let u', hu = sh_instance u in
(Construct (sh_construct c, u'),
- combinesmall 11 (combine (constructor_syntactic_hash c) hu))
+ combinesmall 11 (combine (constructor_hash c) hu))
| Case (ci,p,c,bl) ->
let p, hp = sh_rec p
and c, hc = sh_rec c in
@@ -928,7 +930,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 eq ci ci' =
+ let equal 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 *)
@@ -970,7 +972,7 @@ module Hsorts =
let hashcons huniv = function
Prop c -> Prop c
| Type u -> Type (huniv u)
- let eq s1 s2 =
+ let equal 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 9849f156c..be71bd7b4 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.SyntacticOrd.equal c1 c2
- | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
- | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
+ | 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
| _ -> false
open Hashset.Combine
let hash = function
- | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
- | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
- | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
+ | ConstRef c -> combinesmall 1 (Constant.hash c)
+ | IndRef i -> combinesmall 2 (ind_hash i)
+ | ConstructRef c -> combinesmall 3 (constructor_hash c)
end
module RefTable = Hashtbl.Make(RefHash)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 109e3830c..30b28177c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val
let pop_rel_context n env =
let ctxt = env.env_rel_context in
{ env with
- env_rel_context = List.skipn n ctxt;
+ env_rel_context = List.firstn (List.length ctxt - n) ctxt;
env_nb_rel = env.env_nb_rel - n }
let fold_named_context f env ~init =
diff --git a/kernel/names.ml b/kernel/names.ml
index a99702d15..ae2b3b638 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -102,7 +102,7 @@ struct
let hashcons hident = function
| Name id -> Name (hident id)
| n -> n
- let eq n1 n2 =
+ let equal n1 n2 =
n1 == n2 ||
match (n1,n2) with
| (Name id1, Name id2) -> id1 == id2
@@ -236,7 +236,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 eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+ let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
(x == y) ||
(Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
let hash = hash
@@ -327,7 +327,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 eq d1 d2 =
+ let rec equal d1 d2 =
d1 == d2 ||
match d1,d2 with
| MPfile dir1, MPfile dir2 -> dir1 == dir2
@@ -423,7 +423,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 eq kn1 kn2 =
+ let equal kn1 kn2 =
kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
kn1.knlabel == kn2.knlabel
let hash = hash
@@ -477,7 +477,7 @@ module KerPair = struct
| Dual (kn,_) -> kn
let same kn = Same kn
- let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
+ let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
let make1 = same
let make2 mp l = same (KerName.make2 mp l)
@@ -524,23 +524,6 @@ 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
@@ -552,7 +535,7 @@ module KerPair = struct
let hashcons hkn = function
| Same kn -> Same (hkn kn)
| Dual (knu,knc) -> make (hkn knu) (hkn knc)
- let eq x y = (* physical comparison on subterms *)
+ let equal x y = (* physical comparison on subterms *)
x == y ||
match x,y with
| Same x, Same y -> x == y
@@ -607,8 +590,6 @@ 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
@@ -616,22 +597,15 @@ 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
@@ -639,16 +613,11 @@ 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
@@ -693,7 +662,7 @@ module Hind = Hashcons.Make(
type t = inductive
type u = MutInd.t -> MutInd.t
let hashcons hmind (mind, i) = (hmind mind, i)
- let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
+ let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
let hash = ind_hash
end)
@@ -702,7 +671,7 @@ module Hconstruct = Hashcons.Make(
type t = constructor
type u = inductive -> inductive
let hashcons hind (ind, j) = (hind ind, j)
- let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
+ let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
let hash = constructor_hash
end)
@@ -836,22 +805,13 @@ 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 eq ((c,b) as x) ((c',b') as y) =
+ let equal ((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 9a8977c92..7cc444375 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -305,12 +305,6 @@ 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] *)
@@ -385,12 +379,6 @@ 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] *)
@@ -429,22 +417,16 @@ 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_hash : constructor -> int
val constructor_user_ord : constructor -> constructor -> int
+val constructor_hash : 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 =
@@ -658,12 +640,6 @@ 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 2baf9b133..e2854abfd 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 eq s1 s2 = match (s1,s2) with
+ let equal 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 09a64d1b0..336cdb653 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -35,7 +35,7 @@ module type Hashconsed =
sig
type t
val hash : t -> int
- val eq : t -> t -> bool
+ val equal : 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 eq l1 l2 = match l1, l2 with
+ let equal 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.eq x y then l
+ if H.equal x y then l
else cons y (remove x l)
let rec mem x = function
| Nil -> false
- | Cons (y, _, l) -> H.eq x y || mem x l
+ | Cons (y, _, l) -> H.equal 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 eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+ let equal 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
@@ -398,7 +398,7 @@ struct
let hashcons hdir (b,n as x) =
let b' = hdir b in
if b' == b then x else (b',n)
- let eq l1 l2 =
+ let equal l1 l2 =
l1 == l2 ||
match l1,l2 with
| (b,n), (b',n') -> b == b' && n == n'
@@ -417,7 +417,7 @@ struct
let hcons =
Hashcons.simple_hcons H.generate H.hcons Level.hcons
let hash = ExprHash.hash
- let eq x y = x == y ||
+ let equal x y = x == y ||
(let (u,n) = x and (v,n') = y in
Int.equal n n' && Level.equal u v)
@@ -1293,7 +1293,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 eq (l1,k,l2) (l1',k',l2') =
+ let equal (l1,k,l2) (l1',k',l2') =
l1 == l1' && k == k' && l2 == l2'
let hash = Hashtbl.hash
end)
@@ -1305,7 +1305,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 eq s s' =
+ let equal s s' =
List.for_all2eq (==)
(Constraint.elements s)
(Constraint.elements s')
@@ -1676,7 +1676,7 @@ struct
a
end
- let eq t1 t2 =
+ let equal t1 t2 =
t1 == t2 ||
(Int.equal (Array.length t1) (Array.length t2) &&
let rec aux i =
@@ -2043,7 +2043,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 eq s s' =
+ let equal s s' =
LSet.equal s s'
let hash = Hashtbl.hash
end)
diff --git a/lib/cSet.ml b/lib/cSet.ml
index 783165630..d7d5c70b3 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 eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
+ let equal 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 d368e20e6..46ba0b628 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.
- * [eq] is a comparison function. It is allowed to use physical equality
+ * [equal] 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 eq : t -> t -> bool
+ val equal : 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.eq. This is
+ * w.r.t (=), although the equality on keys is X.equal. This is
* granted since we hcons the subterms before looking up in the table.
*)
module Htbl = Hashset.Make(X)
@@ -124,7 +124,7 @@ module Hlist (D:HashedType) =
let hashcons (hrec,hdata) = function
| x :: l -> hdata x :: hrec l
| l -> l
- let eq l1 l2 =
+ let equal l1 l2 =
l1 == l2 ||
match l1, l2 with
| [], [] -> true
@@ -144,7 +144,7 @@ module Hstring = Make(
type t = string
type u = unit
let hashcons () s =(* incr accesstr;*) s
- external eq : string -> string -> bool = "caml_string_equal" "noalloc"
+ external equal : string -> string -> bool = "caml_string_equal" "noalloc"
(** Copy from CString *)
let rec hash len s i accu =
if i = len then accu
@@ -191,7 +191,7 @@ module Hobj = Make(
type t = Obj.t
type u = (Obj.t -> Obj.t) * unit
let hashcons (hrec,_) = hash_obj hrec
- let eq = comp_obj
+ let equal = comp_obj
let hash = Hashtbl.hash
end)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 93890c494..8d0adc3fd 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 [eq], a hashconsing function is a
+ Given an equivalence relation [equal], a hashconsing function is a
function that associates the same canonical element to two elements
- related by [eq]. Usually, the element chosen is canonical w.r.t.
+ related by [equal]. 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 [eq], that is
- [eq x (hashcons f x) = true]. *)
- val eq : t -> t -> bool
+ hashcons substructures. It should be compatible with [equal], that is
+ [equal x (hashcons f x) = true]. *)
+ val equal : 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 [eq], i.e. if [eq x y = true] then
+ should be compatible with [equal], i.e. if [equal x y = true] then
[hash x = hash y]. *)
end
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 9454aef9b..1ca6cc641 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -16,7 +16,7 @@
module type EqType = sig
type t
- val eq : t -> t -> bool
+ val equal : 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.eq v d -> v
+ | Some v when E.equal v d -> v
| _ -> loop (i + 1)
end else loop (i + 1)
in
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 270484d8a..a455eec66 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -16,7 +16,7 @@
module type EqType = sig
type t
- val eq : t -> t -> bool
+ val equal : t -> t -> bool
end
type statistics = {
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b73ff2bc5..bb07bf056 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -380,26 +380,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
let consume_stack on_left (termF,skF) (termO,skO) evd =
let switch f a b = if on_left then f a b else f b a in
- let not_only_appO = Stack.not_purely_applicative skO in
- match switch (ise_stack2 not_only_appO env evd (evar_conv_x ts)) skF skO with
- |Some (lF,rO), Success i' when on_left && (not_only_appO || List.is_empty lF) ->
- (* Case (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *)
- (* or (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *)
- switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO))
- |Some (rO,lF), Success i' when not on_left && (not_only_appO || List.is_empty lF) ->
- switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO))
+ let not_only_app = Stack.not_purely_applicative skO in
+ match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
+ |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
+ switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
+ |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
+ switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
|None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
|_, (UnifFailure _ as x) -> x
|Some _, _ -> UnifFailure (evd,NotSameArgSize) in
- let eta env evd onleft (termR,skR) (termO,skO) =
- assert (match skR with [] -> true | _ -> false);
- let (na,c1,c'1) = destLambda termR in
+ let eta env evd onleft sk term sk' term' =
+ assert (match sk with [] -> true | _ -> false);
+ let (na,c1,c'1) = destLambda term in
let c = nf_evar evd c1 in
let env' = push_rel (na,None,c) env in
let out1 = whd_betaiota_deltazeta_for_iota_state
(fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
let out2 = whd_nored_state evd
- (Stack.zip (termO, skO @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty),
+ (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty),
Cst_stack.empty in
if onleft then evar_eqappr_x ts env' evd CONV out1 out2
else evar_eqappr_x ts env' evd CONV out2 out1
@@ -419,7 +417,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let not_only_app = Stack.not_purely_applicative skM in
let f1 i =
match Stack.list_of_app_stack skF with
- | None -> quick_fail evd
+ | None -> default_fail evd
| Some lF ->
let tM = Stack.zip apprM in
miller_pfenning on_left
@@ -427,9 +425,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM
else quick_fail i)
ev lF tM i
- and consume (termF,skF as apprF) (termM,skM as apprM) i =
+ and consume (termF,skF as apprF) (termM,skM as apprM) i =
if not (Stack.is_empty skF && Stack.is_empty skM) then
- (* This tries first-order matching *)
consume_stack on_left apprF apprM i
else quick_fail i
and delta i =
@@ -468,32 +465,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let switch f a b = if on_left then f a b else f b a in
let eta evd =
match kind_of_term termR with
- | Lambda _ -> eta env evd false apprR apprF
- | Construct u -> eta_constructor ts env evd (u,skR) apprF
+ | Lambda _ -> eta env evd false skR termR skF termF
+ | Construct u -> eta_constructor ts env evd skR u skF termF
| _ -> UnifFailure (evd,NotSameHead)
in
- let postpone tR lF evd =
- (* Postpone the use of an heuristic *)
- if not (occur_rigidly (fst ev) evd tR) then
- let evd,tF =
- if isRel tR || isVar tR then
- (* Optimization so as to generate candidates *)
- let evd,ev = evar_absorb_arguments env evd ev lF in
- evd,mkEvar ev
- else
- evd,Stack.zip apprF in
- switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) evd))
- tF tR
- else
- UnifFailure (evd,OccurCheck (fst ev,tR))
- in
match Stack.list_of_app_stack skF with
| None ->
ise_try evd [consume_stack on_left apprF apprR; eta]
| Some lF ->
let tR = Stack.zip apprR in
miller_pfenning on_left
- (fun () -> ise_try evd [eta;postpone tR lF])
+ (fun () ->
+ ise_try evd
+ [eta;(* Postpone the use of an heuristic *)
+ (fun i ->
+ if not (occur_rigidly (fst ev) i tR) then
+ let i,tF =
+ if isRel tR || isVar tR then
+ (* Optimization so as to generate candidates *)
+ let i,ev = evar_absorb_arguments env i ev lF in
+ i,mkEvar ev
+ else
+ i,Stack.zip apprF in
+ switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
+ tF tR
+ else
+ UnifFailure (evd,OccurCheck (fst ev,tR)))])
ev lF tR evd
in
let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
@@ -712,10 +709,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* Eta-expansion *)
| Rigid, _ when isLambda term1 ->
- eta env evd true appr1 appr2
+ eta env evd true sk1 term1 sk2 term2
| _, Rigid when isLambda term2 ->
- eta env evd false appr2 appr1
+ eta env evd false sk2 term2 sk1 term1
| Rigid, Rigid -> begin
match kind_of_term term1, kind_of_term term2 with
@@ -755,10 +752,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
rigids env evd sk1 term1 sk2 term2
| Construct u, _ ->
- eta_constructor ts env evd (u,sk1) appr2
+ eta_constructor ts env evd sk1 u sk2 term2
| _, Construct u ->
- eta_constructor ts env evd (u,sk2) appr1
+ eta_constructor ts env evd sk2 u sk1 term1
| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -854,7 +851,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
(fst (decompose_app_vect (substl ks h))))]
else UnifFailure(evd,(*dummy*)NotSameHead)
-and eta_constructor ts env evd (((ind, i), u),sk1) (term2,sk2) =
+and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
| Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2892de7c4..dc70f36cc 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -306,9 +306,7 @@ struct
| Update t -> str "ZUpdate(" ++ pr_c t ++ str ")"
and pr pr_c l =
let open Pp in
- str "[" ++
- prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l ++
- str "]"
+ prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
and pr_cst_member pr_c c =
let open Pp in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 51df07f28..1df2a73b2 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -90,9 +90,6 @@ module Stack : sig
val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
val not_purely_applicative : 'a t -> bool
-
- (** @return the arguments in the stack if a purely applicative
- stack, None otherwise *)
val list_of_app_stack : constr t -> constr list option
val assign : 'a t -> int -> 'a -> 'a t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index bde0a1c16..d024c01ba 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -145,12 +145,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
delete_current_proof ();
iraise reraise
-let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
+let build_by_tactic env ctx ?(poly=false) typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
let gk = Global, poly, Proof Theorem in
let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
- let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in
+ let ce = Term_typing.handle_entry_side_effects env ce in
let (cb, ctx), se = Future.force ce.const_entry_body in
assert(Declareops.side_effects_is_empty se);
assert(Univ.ContextSet.is_empty ctx);
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 4aa3c3bfd..5e0fb4dd3 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -153,7 +153,7 @@ val build_constant_by_tactic :
types -> unit Proofview.tactic ->
Entries.definition_entry * bool * Evd.evar_universe_context
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
+val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic ->
types -> unit Proofview.tactic ->
constr * bool * Evd.evar_universe_context
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index dbaa60d61..749e0d2b5 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -21,7 +21,7 @@ open Ind_tables
(* Induction/recursion schemes *)
-let optimize_non_type_induction_scheme kind dep sort _ ind =
+let optimize_non_type_induction_scheme kind dep sort ind =
let env = Global.env () in
let sigma = Evd.from_env env in
if check_scheme kind ind then
@@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind =
let rect_scheme_kind_from_type =
declare_individual_scheme_object "_rect_nodep"
- (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+ (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
let rect_scheme_kind_from_prop =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
- (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+ (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
let rect_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
- (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
+ (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
let ind_scheme_kind_from_type =
declare_individual_scheme_object "_ind_nodep"
@@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
let case_scheme_kind_from_type =
declare_individual_scheme_object "_case_nodep"
- (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+ (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
let case_scheme_kind_from_prop =
declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
- (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+ (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
let case_dep_scheme_kind_from_type =
declare_individual_scheme_object "_case" ~aux:"_case_from_type"
- (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+ (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
let case_dep_scheme_kind_from_type_in_prop =
declare_individual_scheme_object "_casep_dep"
- (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+ (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
let case_dep_scheme_kind_from_prop =
declare_individual_scheme_object "_case_dep"
- (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+ (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
let case_dep_scheme_kind_from_prop_in_prop =
declare_individual_scheme_object "_casep"
- (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+ (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f7d3ad5d0..8643fe10f 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -191,7 +191,7 @@ let build_sym_scheme env ind =
let sym_scheme_kind =
declare_individual_scheme_object "_sym_internal"
- (fun _ ind ->
+ (fun ind ->
let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
(c, ctx), Declareops.no_seff)
@@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind =
let sym_involutive_scheme_kind =
declare_individual_scheme_object "_sym_involutive"
- (fun _ ind ->
+ (fun ind ->
build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
(**********************************************************************)
@@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme
(**********************************************************************)
let rew_l2r_dep_scheme_kind =
declare_individual_scheme_object "_rew_r_dep"
- (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
+ (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
(**********************************************************************)
(* Dependent rewrite from right-to-left in conclusion *)
@@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_dep_scheme_kind =
declare_individual_scheme_object "_rew_dep"
- (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+ (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
(**********************************************************************)
(* Dependent rewrite from right-to-left in hypotheses *)
@@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_dep"
- (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+ (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
(**********************************************************************)
(* Dependent rewrite from left-to-right in hypotheses *)
@@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind =
(**********************************************************************)
let rew_l2r_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_r_dep"
- (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+ (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
(**********************************************************************)
(* Non-dependent rewrite from either left-to-right in conclusion or *)
@@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind =
(**********************************************************************)
let rew_l2r_scheme_kind =
declare_individual_scheme_object "_rew_r"
- (fun _ ind -> fix_r2l_forward_rew_scheme
+ (fun ind -> fix_r2l_forward_rew_scheme
(build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
(**********************************************************************)
@@ -704,7 +704,7 @@ let rew_l2r_scheme_kind =
(**********************************************************************)
let rew_r2l_scheme_kind =
declare_individual_scheme_object "_rew"
- (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
+ (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
(* End of rewriting schemes *)
@@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind =
in c, Evd.evar_universe_context_of ctx
let congr_scheme_kind = declare_individual_scheme_object "_congr"
- (fun _ ind ->
+ (fun ind ->
(* May fail if equality is not defined *)
build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 074004fa1..24d5cf8a9 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -371,7 +371,7 @@ Qed.
Goal True.
Fail eapply existT.
-Set Universal Lemma Under Conjunction.
+Set Trivial Tactic Unification Under Conjunction.
eapply existT.
Abort.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 07d7f9150..a7bdba90a 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -69,9 +69,6 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
Reserved Notation "{ x | P }" (at level 0, x at level 99).
Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
-Reserved Notation "{ x & P }" (at level 0, x at level 99).
-Reserved Notation "{ x & P & Q }" (at level 0, x at level 99).
-
Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index ecdbef7f6..1384901b7 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -48,8 +48,6 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
-Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.
-Notation "{ x & P & Q }" := (sigT2 (fun x => P) (fun x => Q)) : type_scope.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 118ffb3e8..d1452fca2 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -111,7 +111,7 @@ let check_bool_is_defined () =
let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
-let build_beq_scheme mode kn =
+let build_beq_scheme kn =
check_bool_is_defined ();
(* fetching global env *)
let env = Global.env() in
@@ -188,7 +188,7 @@ let build_beq_scheme mode kn =
else begin
try
let eq, eff =
- let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in
+ let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in
mkConst c, eff in
let eqa, eff =
let eqa, effs = List.split (List.map aux a) in
@@ -330,7 +330,7 @@ let destruct_ind c =
so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
*)
(* used in the leib -> bool side*)
-let do_replace_lb mode lb_scheme_key aavoid narg p q =
+let do_replace_lb lb_scheme_key aavoid narg p q =
let avoid = Array.of_list aavoid in
let do_arg v offset =
try
@@ -360,7 +360,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
try
- let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in
+ let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in
Proofview.tclUNIT (mkConst c, eff)
with Not_found ->
(* spiwack: the format of this error message should probably
@@ -388,7 +388,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
end
(* used in the bool -> leib side *)
-let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let avoid = Array.of_list aavoid in
let do_arg v offset =
try
@@ -551,7 +551,7 @@ let compute_bl_goal ind lnamesparrec nparrec =
(mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
))), eff
-let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
+let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let avoid = ref [] in
let first_intros =
@@ -608,7 +608,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
if eq_gr (IndRef indeq) Coqlib.glob_eq
then
Tacticals.New.tclTHEN
- (do_replace_bl mode bl_scheme_key ind
+ (do_replace_bl bl_scheme_key ind
(!avoid)
nparrec (ca.(2))
(ca.(1)))
@@ -625,12 +625,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
-let side_effect_of_mode = function
- | Declare.KernelVerbose -> false
- | Declare.KernelSilent -> true
- | Declare.UserVerbose -> false
-
-let make_bl_scheme mode mind =
+let make_bl_scheme mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
errorlabstrm ""
@@ -642,9 +637,8 @@ let make_bl_scheme mode mind =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in
- let side_eff = side_effect_of_mode mode in
- let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
- (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
+ let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal
+ (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
in
([|ans|], ctx), eff
@@ -694,7 +688,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
))), eff
-let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
+let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let avoid = ref [] in
let first_intros =
@@ -738,7 +732,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
| App(c,ca) -> (match (kind_of_term ca.(1)) with
| App(c',ca') ->
let n = Array.length ca' in
- do_replace_lb mode lb_scheme_key
+ do_replace_lb lb_scheme_key
(!avoid)
nparrec
ca'.(n-2) ca'.(n-1)
@@ -753,7 +747,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
-let make_lb_scheme mode mind =
+let make_lb_scheme mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
errorlabstrm ""
@@ -765,9 +759,8 @@ let make_lb_scheme mode mind =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
let ctx = Evd.empty_evar_universe_context in
- let side_eff = side_effect_of_mode mode in
- let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
- (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
+ let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal
+ (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
in
([|ans|], ctx (* FIXME *)), eff
@@ -926,7 +919,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
]
end
-let make_eq_decidability mode mind =
+let make_eq_decidability mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
raise DecidabilityMutualNotSupported;
@@ -937,8 +930,7 @@ let make_eq_decidability mode mind =
let ctx = Evd.empty_evar_universe_context (* FIXME *)in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- let side_eff = side_effect_of_mode mode in
- let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx
+ let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx
(compute_dec_goal (ind,u) lnamesparrec nparrec)
(compute_dec_tact ind lnamesparrec nparrec)
in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index b59d6fc8a..0d39466ed 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -28,10 +28,11 @@ open Pp
(**********************************************************************)
(* Registering schemes in the environment *)
+
type mutual_scheme_object_function =
- internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+ mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+ inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
type 'a scheme_kind = string
@@ -140,31 +141,32 @@ let define internal id c p univs =
in
kn
-let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
- let (c, ctx), eff = f mode ind in
+let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
+ let (c, ctx), eff = f ind in
let mib = Global.lookup_mind mind in
let id = match idopt with
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
- let const = define mode id c mib.mind_polymorphic ctx in
+ let const = define internal id c mib.mind_polymorphic ctx in
declare_scheme kind [|ind,const|];
const, Declareops.cons_side_effects
(Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
-let define_individual_scheme kind mode names (mind,i as ind) =
+let define_individual_scheme kind internal names (mind,i as ind) =
match Hashtbl.find scheme_object_table kind with
| _,MutualSchemeFunction f -> assert false
| s,IndividualSchemeFunction f ->
- define_individual_scheme_base kind s f mode names ind
+ define_individual_scheme_base kind s f internal names ind
-let define_mutual_scheme_base kind suff f mode names mind =
- let (cl, ctx), eff = f mode mind in
+let define_mutual_scheme_base kind suff f internal names mind =
+ let (cl, ctx), eff = f mind in
let mib = Global.lookup_mind mind in
let ids = Array.init (Array.length mib.mind_packets) (fun i ->
try Int.List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
+
let consts = Array.map2 (fun id cl ->
- define mode id cl mib.mind_polymorphic ctx) ids cl in
+ define internal id cl mib.mind_polymorphic ctx) ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
declare_scheme kind schemes;
consts,
@@ -173,11 +175,11 @@ let define_mutual_scheme_base kind suff f mode names mind =
kind (Global.safe_env()) (Array.to_list schemes))
eff
-let define_mutual_scheme kind mode names mind =
+let define_mutual_scheme kind internal names mind =
match Hashtbl.find scheme_object_table kind with
| _,IndividualSchemeFunction _ -> assert false
| s,MutualSchemeFunction f ->
- define_mutual_scheme_base kind s f mode names mind
+ define_mutual_scheme_base kind s f internal names mind
let find_scheme_on_env_too kind ind =
let s = String.Map.find kind (Indmap.find ind !scheme_map) in
@@ -186,14 +188,14 @@ let find_scheme_on_env_too kind ind =
kind (Global.safe_env()) [ind, s])
Declareops.no_seff
-let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) =
+let find_scheme kind (mind,i as ind) =
try find_scheme_on_env_too kind ind
with Not_found ->
match Hashtbl.find scheme_object_table kind with
| s,IndividualSchemeFunction f ->
- define_individual_scheme_base kind s f mode None ind
+ define_individual_scheme_base kind s f KernelSilent None ind
| s,MutualSchemeFunction f ->
- let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
+ let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in
ca.(i), eff
let check_scheme kind ind =
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index d0844dd94..98eaac092 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -8,7 +8,6 @@
open Term
open Names
-open Declare
(** This module provides support for registering inductive scheme builders,
declaring schemes and generating schemes on demand *)
@@ -20,9 +19,9 @@ type individual
type 'a scheme_kind
type mutual_scheme_object_function =
- internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+ mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+ inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
(** Main functions to register a scheme builder *)
@@ -33,17 +32,21 @@ val declare_individual_scheme_object : string -> ?aux:string ->
individual_scheme_object_function ->
individual scheme_kind
+(*
+val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
+*)
+
(** Force generation of a (mutually) scheme with possibly user-level names *)
val define_individual_scheme : individual scheme_kind ->
- internal_flag (** internal *) ->
+ Declare.internal_flag (** internal *) ->
Id.t option -> inductive -> constant * Declareops.side_effects
-val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
+val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
(int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects
(** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects
+val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects
val check_scheme : 'a scheme_kind -> inductive -> bool
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 23:12:07 +0000