aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES4
-rw-r--r--contrib/correctness/ptactic.ml4
-rw-r--r--contrib/xml/doubleTypeInference.ml2
-rw-r--r--contrib/xml/proof2aproof.ml2
-rw-r--r--dev/db1
-rw-r--r--pretyping/evarutil.ml21
-rw-r--r--pretyping/evd.ml24
-rw-r--r--pretyping/evd.mli7
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/reductionops.ml6
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/refiner.ml2
-rw-r--r--tactics/evar_tactics.ml2
-rw-r--r--tactics/tacinterp.ml4
-rw-r--r--theories/Logic/ClassicalChoice.v2
16 files changed, 46 insertions, 45 deletions
diff --git a/CHANGES b/CHANGES
index b094d8ffb..3f4cf0aa4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -96,9 +96,11 @@ Notations
- no more automatic printing box in case of user-provided printing "format".
- new notation "exists! x:A, P" for unique existence.
-Library
+Libraries
- Small extension of Zmin.V, new Zmax.v, new Zminmax.v
+- Reworking of the files on classical logic and description principles
+ (possible incompatibilities)
- New library on String and Ascii characters (contributed by L. Thery)
- Few other improvements in ZArith potentially exceptionally breaking the
compatibility (useless hypothesys of Zgt_square_simpl and
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 5994fb38d..e7610923c 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -208,8 +208,8 @@ let reduce_open_constr (em0,c) =
| Cast (c',t) ->
(match kind_of_term c' with
| Evar (ev,_) ->
- if not (Evd.in_dom em ev) then
- Evd.add em ev (Evd.map em0 ev)
+ if not (Evd.mem em ev) then
+ Evd.add em ev (Evd.find em0 ev)
else
em
| _ -> fold_constr collect em c)
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 518f6c115..a3336817e 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -93,7 +93,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
let jty = execute env sigma ty None in
let jty = assumption_of_judgment env sigma jty in
let evar_context =
- E.named_context_of_val (Evd.map sigma n).Evd.evar_hyps in
+ E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in
let rec iter actual_args evar_context =
match actual_args,evar_context with
[],[] -> ()
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index dff546c94..678b650cc 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -47,7 +47,7 @@ let nf_evar sigma ~preserve =
| _ -> T.mkApp (c', l')
)
| _ -> T.mkApp (c', l'))
- | T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e ->
+ | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e ->
aux (Evd.existential_value sigma (e,l))
| T.Evar (e,l) -> T.mkEvar (e, Array.map aux l)
| T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl)
diff --git a/dev/db b/dev/db
index 6c657d4ed..784e5bac8 100644
--- a/dev/db
+++ b/dev/db
@@ -28,6 +28,7 @@ install_printer Top_printers.ppgoal
install_printer Top_printers.ppsigmagoal
install_printer Top_printers.pproof
install_printer Top_printers.ppevd
+install_printer Top_printers.ppevm
install_printer Top_printers.ppclenv
install_printer Top_printers.pptac
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2785d0838..658bf407f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -35,7 +35,7 @@ exception Uninstantiated_evar of existential_key
let rec whd_ise sigma c =
match kind_of_term c with
- | Evar (ev,args) when Evd.in_dom sigma ev ->
+ | Evar (ev,args) when Evd.mem sigma ev ->
if Evd.is_defined sigma ev then
whd_ise sigma (existential_value sigma (ev,args))
else raise (Uninstantiated_evar ev)
@@ -46,7 +46,7 @@ let rec whd_ise sigma c =
let whd_castappevar_stack sigma c =
let rec whrec (c, l as s) =
match kind_of_term c with
- | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+ | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev ->
whrec (existential_value sigma (ev,args), l)
| Cast (c,_,_) -> whrec (c, l)
| App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
@@ -93,7 +93,7 @@ let collect_evars emap c =
let rec collrec acc c =
match kind_of_term c with
| Evar (k,_) ->
- if Evd.in_dom emap k & not (Evd.is_defined emap k) then k::acc
+ if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc
else (* No recursion on the evar instantiation *) acc
| _ ->
fold_constr collrec acc c in
@@ -103,13 +103,14 @@ let push_dependent_evars sigma emap =
Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
List.fold_left
(fun (sigma',emap') ev ->
- (Evd.add sigma' ev (Evd.map emap' ev),Evd.rmv emap' ev))
+ (Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
(sigma',emap') (collect_evars emap' ccl))
emap (sigma,emap)
(* replaces a mapping of existentials into a mapping of metas.
Problem if an evar appears in the type of another one (pops anomaly) *)
let evars_to_metas sigma (emap, c) =
+ let emap = nf_evars emap in
let sigma',emap' = push_dependent_evars sigma emap in
let change_exist evar =
let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
@@ -117,7 +118,7 @@ let evars_to_metas sigma (emap, c) =
mkCast (mkMeta n, DEFAULTcast, ty) in
let rec replace c =
match kind_of_term c with
- Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev
+ Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev
| _ -> map_constr replace c in
(sigma', replace c)
@@ -297,7 +298,7 @@ let is_defined_equation env evd (ev,inst) rhs =
is_pattern inst &&
not (occur_evar ev rhs) &&
try
- let evi = Evd.map (evars_of evd) ev in
+ let evi = Evd.find (evars_of evd) ev in
let (evd',body) = inverse_instance env evd ev evi inst rhs in
evar_well_typed_body evd' ev evi body
with Failure _ -> false
@@ -313,7 +314,7 @@ let is_defined_equation env evd (ev,inst) rhs =
let do_restrict_hyps evd ev args =
let args = Array.to_list args in
- let evi = Evd.map (evars_of !evd) ev in
+ let evi = Evd.find (evars_of !evd) ev in
let env = evar_env evi in
let hyps = evar_context evi in
let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
@@ -395,7 +396,7 @@ let evar_define env (ev,argsv) rhs isevars =
if occur_evar ev rhs
then error_occur_check env (evars_of isevars) ev rhs;
let args = Array.to_list argsv in
- let evi = Evd.map (evars_of isevars) ev in
+ let evi = Evd.find (evars_of isevars) ev in
(* the bindings to invert *)
let worklist = make_subst (evar_env evi) args in
let (isevars',body) = real_clean env isevars ev evi worklist rhs in
@@ -502,7 +503,7 @@ let status_changed lev (pbty,t1,t2) =
let solve_refl conv_algo env isevars ev argsv1 argsv2 =
if argsv1 = argsv2 then (isevars,[]) else
- let evd = Evd.map (evars_of isevars) ev in
+ let evd = Evd.find (evars_of isevars) ev in
let hyps = evar_context evd in
let (isevars',_,rsign) =
array_fold_left2
@@ -599,7 +600,7 @@ let mk_valcon c = Some c
cumulativity now includes Prop and Set in Type...
It is, but that's not too bad *)
let define_evar_as_abstraction abs evd (ev,args) =
- let evi = Evd.map (evars_of evd) ev in
+ let evi = Evd.find (evars_of evd) ev in
let evenv = evar_env evi in
let (evd1,dom) = new_evar evd evenv (new_Type()) in
let nvar =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5da0a1a99..713995641 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -48,17 +48,16 @@ let empty = Evarmap.empty
let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
-let map evc k = Evarmap.find k evc
-let rmv evc k = Evarmap.remove k evc
-let remap evc k i = Evarmap.add k i evc
-let in_dom evc k = Evarmap.mem k evc
+let find evc k = Evarmap.find k evc
+let remove evc k = Evarmap.remove k evc
+let mem evc k = Evarmap.mem k evc
let fold = Evarmap.fold
let add evd ev newinfo = Evarmap.add ev newinfo evd
let define evd ev body =
let oldinfo =
- try map evd ev
+ try find evd ev
with Not_found -> error "Evd.define: cannot define undeclared evar" in
let newinfo =
{ evar_concl = oldinfo.evar_concl;
@@ -68,10 +67,10 @@ let define evd ev body =
| Evar_empty -> Evarmap.add ev newinfo evd
| _ -> anomaly "Evd.define: cannot define an isevar twice"
-let is_evar sigma ev = in_dom sigma ev
+let is_evar sigma ev = mem sigma ev
let is_defined sigma ev =
- let info = map sigma ev in
+ let info = find sigma ev in
not (info.evar_body = Evar_empty)
let evar_body ev = ev.evar_body
@@ -112,7 +111,7 @@ let instantiate_evar sign c args =
let existential_type sigma (n,args) =
let info =
- try map sigma n
+ try find sigma n
with Not_found ->
anomaly ("Evar "^(string_of_existential n)^" was not declared") in
let hyps = evar_context info in
@@ -121,7 +120,7 @@ let existential_type sigma (n,args) =
exception NotInstantiatedEvar
let existential_value sigma (n,args) =
- let info = map sigma n in
+ let info = find sigma n in
let hyps = evar_context info in
match evar_body info with
| Evar_defined c ->
@@ -270,10 +269,9 @@ type evar_map = evar_map1 * sort_constraints
let empty = empty, UniverseMap.empty
let add (sigma,sm) k v = (add sigma k v, sm)
let dom (sigma,_) = dom sigma
-let map (sigma,_) = map sigma
-let rmv (sigma,sm) k = (rmv sigma k, sm)
-let remap (sigma,sm) k v = (remap sigma k v, sm)
-let in_dom (sigma,_) = in_dom sigma
+let find (sigma,_) = find sigma
+let remove (sigma,sm) k = (remove sigma k, sm)
+let mem (sigma,_) = mem sigma
let to_list (sigma,_) = to_list sigma
let fold f (sigma,_) = fold f sigma
let define (sigma,sm) k v = (define sigma k v, sm)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 35bcb67c7..6481ff201 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -43,10 +43,9 @@ val empty : evar_map
val add : evar_map -> evar -> evar_info -> evar_map
val dom : evar_map -> evar list
-val map : evar_map -> evar -> evar_info
-val rmv : evar_map -> evar -> evar_map
-val remap : evar_map -> evar -> evar_info -> evar_map
-val in_dom : evar_map -> evar -> bool
+val find : evar_map -> evar -> evar_info
+val remove : evar_map -> evar -> evar_map
+val mem : evar_map -> evar -> bool
val to_list : evar_map -> (evar * evar_info) list
val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 82a45ad44..01841641c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -273,7 +273,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| REvar (loc, ev, instopt) ->
(* Ne faudrait-il pas s'assurer que hyps est bien un
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
- let hyps = evar_context (Evd.map (evars_of !isevars) ev) in
+ let hyps = evar_context (Evd.find (evars_of !isevars) ev) in
let args = match instopt with
| None -> instance_from_named_context hyps
| Some inst -> failwith "Evar subtitutions not implemented" in
@@ -657,8 +657,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let rec proc_rec c =
match kind_of_term c with
| Evar (ev,args) ->
- assert (Evd.in_dom sigma ev);
- if not (Evd.in_dom initial_sigma ev) then
+ assert (Evd.mem sigma ev);
+ if not (Evd.mem initial_sigma ev) then
let (loc,k) = evar_source ev !isevars in
error_unsolvable_implicit loc env sigma k
| _ -> iter_constr proc_rec c
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 20b48a01a..9a0125025 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -428,13 +428,13 @@ let whd_betadeltaiota_nolet env sigma x =
let rec whd_evar sigma c =
match kind_of_term c with
| Evar (ev,args)
- when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+ when Evd.mem sigma ev & Evd.is_defined sigma ev ->
whd_evar sigma (Evd.existential_value sigma (ev,args))
| Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
| _ -> collapse_appl c
-let nf_evar evd =
- local_strong (whd_evar evd)
+let nf_evar sigma =
+ local_strong (whd_evar sigma)
(* lazy reduction functions. The infos must be created for each term *)
let clos_norm_flags flgs env sigma t =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c5d7d672..f231c728b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -259,7 +259,7 @@ let w_merge env with_types mod_delta metas evars evd =
end
and mimick_evar evd mod_delta hdc nargs sp =
- let ev = Evd.map (evars_of evd) sp in
+ let ev = Evd.find (evars_of evd) sp in
let sp_env = Global.env_of_context ev.evar_hyps in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (mc,ec) =
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0f3fa7584..d5ea25bd3 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -25,7 +25,7 @@ open Refiner
let w_refine env ev rawc evd =
if Evd.is_defined (evars_of evd) ev then
error "Instantiate called on already-defined evar";
- let e_info = Evd.map (evars_of evd) ev in
+ let e_info = Evd.find (evars_of evd) ev in
let env = Evd.evar_env e_info in
let sigma,typed_c =
Pretyping.Default.understand_tcc (evars_of evd) env
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 0bb4a9735..ee4b672a1 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -263,7 +263,7 @@ let extract_open_proof sigma pf =
let meta_cnt = ref 0 in
let rec f () =
incr meta_cnt;
- if in_dom sigma (existential_of_int !meta_cnt) then f ()
+ if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
else !meta_cnt
in f
in
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index a321b9f1b..d01cd8ca2 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -23,7 +23,7 @@ open Termops
let evar_list evc c =
let rec evrec acc c =
match kind_of_term c with
- | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+ | Evar (n, _) when Evd.mem evc n -> c :: acc
| _ -> fold_constr evrec acc c
in
evrec [] c
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2eb2d88f4..56aaee4fe 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1194,11 +1194,11 @@ let solve_remaining_evars env initial_sigma evars c =
let isevars = ref evars in
let rec proc_rec c =
match kind_of_term (Reductionops.whd_evar (evars_of !isevars) c) with
- | Evar (ev,args as k) when not (Evd.in_dom initial_sigma ev) ->
+ | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
let (loc,src) = evar_source ev !isevars in
let sigma = evars_of !isevars in
(try
- let evi = Evd.map sigma ev in
+ let evi = Evd.find sigma ev in
let c = solvable_by_tactic env evi k src in
isevars := Evd.evar_define ev c !isevars;
c
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 69887a540..5b347b1be 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -14,7 +14,7 @@
As ClassicalDescription.v, it implies the double-negation of
excluded-middle in Set and implies a strongly classical
world. Especially it conflicts with impredicativity of Set, knowing
- that true<>false in Set.
+ that [true<>false] in Set.
*)
Require Export ClassicalDescription.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 18:15:34 +0000