aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/autoinstance.ml20
-rw-r--r--toplevel/classes.ml16
-rw-r--r--toplevel/command.ml16
-rw-r--r--toplevel/himsg.ml4
-rw-r--r--toplevel/record.ml6
5 files changed, 31 insertions, 31 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 8a9646a17..520f9b631 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -53,15 +53,15 @@ let subst_evar_in_evm evar def evm =
* T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated
* by this definition. *)
-let rec safe_evar_define evm ev c =
+let rec safe_define evm ev c =
if not (closedn (-1) c) then raise Termops.CannotFilter else
-(* msgnl(str"safe_evar_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
+(* msgnl(str"safe_define "++pr_evar_defs evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
let evi = (Evd.find evm ev) in
let define_subst evm sigma =
Util.Intmap.fold
( fun ev (e,c) evm ->
match kind_of_term c with Evar (i,_) when i=ev -> evm | _ ->
- safe_evar_define evm ev (lift (-List.length e) c)
+ safe_define evm ev (lift (-List.length e) c)
) sigma evm in
match evi.evar_body with
| Evd.Evar_defined def ->
@@ -70,7 +70,7 @@ let rec safe_evar_define evm ev c =
let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in
let u = Libtypes.reduce (evar_concl evi) in
let evm = subst_evar_in_evm ev c evm in
- define_subst (Evd.define evm ev c) (Termops.filtering [] Reduction.CUMUL t u)
+ define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u)
let add_gen_ctx (cl,gen,evm) ctx : signature * constr list =
let rec really_new_evar () =
@@ -111,9 +111,9 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
let def = applistc (Libnames.constr_of_global gr) argl in
(* msgnl(str"essayons ?"++Util.pr_int ev++spc()++str":="++spc()
++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*)
- (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*)
+ (*++spc()++str"dans"++spc()++pr_evar_defs evm++spc());*)
try
- let evm = safe_evar_define evm ev def in
+ let evm = safe_define evm ev def in
k (cl,gen,evm);
if sort_is_prop && SubstSet.mem s !substs then raise Exit;
substs := SubstSet.add s !substs
@@ -147,10 +147,10 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit
let tyl = List.map (fun (_,_,t) -> t) ctx in
let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in
let def = applistc c argl in
-(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*)
+(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_defs evm);*)
try
if not (Evd.is_defined evm ev) then
- let evm = safe_evar_define evm ev def in
+ let evm = safe_define evm ev def in
aux evm; k (cl,gen,evm)
with Termops.CannotFilter -> ()
) evl in
@@ -220,7 +220,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature
( fun ctx typ ->
List.iter
(fun ((cl,ev,evm),_,_) ->
-(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*)
+(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_defs evm);*)
smap := Gmapl.add (cl,evm) (ctx,ev) !smap)
(Recordops.methods_matching typ)
) [] deftyp;
@@ -263,7 +263,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
then Evd.remove evm ev,gen
else evm,(ev::gen))
gen (evm,[]) in
-(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*)
+(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_defs evm);*)
let ngen = List.length gen in
let (_,ctx,evm) = List.fold_left
( fun (i,ctx,evm) ev ->
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 081d18292..b6c664020 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -72,7 +72,7 @@ type binder_list = (identifier located * bool * constr_expr) list
(* Calls to interpretation functions. *)
let interp_type_evars evdref env ?(impls=([],[])) typ =
- let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+ let typ' = intern_gen true ~impls ( !evdref) env typ in
let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
@@ -133,7 +133,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
let env = Global.env() in
- let isevars = ref (Evd.create_evar_defs Evd.empty) in
+ let isevars = ref Evd.empty in
let tclass =
match bk with
| Implicit ->
@@ -169,7 +169,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
let env' = push_rel_context ctx' env in
isevars := Evarutil.nf_evar_defs !isevars;
isevars := resolve_typeclasses env !isevars;
- let sigma = Evd.evars_of !isevars in
+ let sigma = !isevars in
let subst = List.map (Evarutil.nf_evar sigma) subst in
if Lib.is_modtype () then
begin
@@ -234,9 +234,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
let term = Termops.it_mkLambda_or_LetIn app ctx' in
isevars := Evarutil.nf_evar_defs !isevars;
let term = Evarutil.nf_isevar !isevars term in
- let evm = Evd.evars_of (undefined_evars !isevars) in
+ let evm = (undefined_evars !isevars) in
Evarutil.check_evars env Evd.empty !isevars termtype;
- if evm = Evd.empty then
+ if Evd.is_empty evm then
declare_instance_constant k pri global imps ?hook id term termtype
else begin
isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
@@ -246,7 +246,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
(fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst
| _ -> assert false);
if props <> [] then
- Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
+ Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *)
(!refine_ref (evm, term));
(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
@@ -266,9 +266,9 @@ let named_of_rel_context l =
let context ?(hook=fun _ -> ()) l =
let env = Global.env() in
- let evars = ref (Evd.create_evar_defs Evd.empty) in
+ let evars = ref Evd.empty in
let (env', fullctx), impls = interp_context_evars evars env l in
- let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in
+ let fullctx = Evarutil.nf_rel_context_evar ( !evars) fullctx in
let ce t = Evarutil.check_evars env Evd.empty !evars t in
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
let ctx = try named_of_rel_context fullctx with _ ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1ab819a5e..50c78d0ed 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -115,7 +115,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
| Some comtyp ->
let ty = generalize_constr_expr comtyp bl in
let b = abstract_constr_expr com bl in
- let evdref = ref (Evd.create_evar_defs Evd.empty) in
+ let evdref = ref Evd.empty in
let ty, impls = interp_type_evars_impls ~evdref env ty in
let b, imps = interp_casted_constr_evars_impls ~evdref env b ty in
let body, typ = nf_isevar !evdref b, nf_isevar !evdref ty in
@@ -509,7 +509,7 @@ let check_all_names_different indl =
if l <> [] then raise (InductiveError (SameNamesOverlap l))
let mk_mltype_data evdref env assums arity indname =
- let is_ml_type = is_sort env (evars_of !evdref) arity in
+ let is_ml_type = is_sort env ( !evdref) arity in
(is_ml_type,indname,assums)
let prepare_param = function
@@ -530,7 +530,7 @@ let interp_cstrs evdref env impls mldata arity ind =
let interp_mutual paramsl indl notations finite =
check_all_names_different indl;
let env0 = Global.env() in
- let evdref = ref (Evd.create_evar_defs Evd.empty) in
+ let evdref = ref Evd.empty in
let (env_params, ctx_params), userimpls =
interp_context_evars ~fail_anonymous:false evdref env0 paramsl
in
@@ -562,7 +562,7 @@ let interp_mutual paramsl indl notations finite =
(* Instantiate evars and check all are resolved *)
let evd,_ = consider_remaining_unif_problems env_params !evdref in
let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
- let sigma = evars_of evd in
+ let sigma = evd in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
let arities = List.map (nf_evar sigma) arities in
@@ -846,12 +846,12 @@ let interp_recursive fixkind l boxed =
let fixnames = List.map (fun fix -> fix.fix_name) fixl in
(* Interp arities allowing for unresolved types *)
- let evdref = ref (Evd.create_evar_defs Evd.empty) in
+ let evdref = ref Evd.empty in
let fixctxs, fiximps =
List.split (List.map (interp_fix_context evdref env) fixl) in
let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
- let fixtypes = List.map (nf_evar (evars_of !evdref)) fixtypes in
+ let fixtypes = List.map (nf_evar ( !evdref)) fixtypes in
let env_rec = push_named_types env fixnames fixtypes in
(* Get interpretation metadatas *)
@@ -867,8 +867,8 @@ let interp_recursive fixkind l boxed =
(* Instantiate evars and check all are resolved *)
let evd,_ = consider_remaining_unif_problems env_rec !evdref in
- let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
- let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
+ let fixdefs = List.map (nf_evar ( evd)) fixdefs in
+ let fixtypes = List.map (nf_evar ( evd)) fixtypes in
let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
List.iter (check_evars env_rec Evd.empty evd) fixdefs;
List.iter (check_evars env Evd.empty evd) fixtypes;
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 42fc6d0fc..e8ca54c9c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -522,10 +522,10 @@ let pr_constraints printenv env evm =
prlist_with_sep (fun () -> fnl ())
(fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l
else
- pr_evar_map evm
+ pr_evar_defs evm
let explain_unsatisfiable_constraints env evd constr =
- let evm = Evd.evars_of evd in
+ let evm = evd in
match constr with
| None ->
str"Unable to satisfy the following constraints:" ++ fnl() ++
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 10d4e5dc6..fe478f080 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -32,7 +32,7 @@ open Topconstr
(********** definition d'un record (structure) **************)
let interp_evars evdref env ?(impls=([],[])) k typ =
- let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+ let typ' = intern_gen true ~impls ( !evdref) env typ in
let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
@@ -64,7 +64,7 @@ let binders_of_decls = List.map binder_of_decl
let typecheck_params_and_fields id t ps nots fs =
let env0 = Global.env () in
- let evars = ref (Evd.create_evar_defs Evd.empty) in
+ let evars = ref Evd.empty in
let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in
let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
@@ -73,7 +73,7 @@ let typecheck_params_and_fields id t ps nots fs =
in
let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in
let evars = Typeclasses.resolve_typeclasses env_ar evars in
- let sigma = Evd.evars_of evars in
+ let sigma = evars in
let newps = Evarutil.nf_rel_context_evar sigma newps in
let newfs = Evarutil.nf_rel_context_evar sigma newfs in
let ce t = Evarutil.check_evars env0 Evd.empty evars t in
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-04 12:48:55 +0000