aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/subtac/equations.ml420
-rw-r--r--contrib/subtac/subtac_cases.ml40
-rw-r--r--contrib/subtac/subtac_classes.ml10
-rw-r--r--contrib/subtac/subtac_coercion.ml46
-rw-r--r--contrib/subtac/subtac_command.ml26
-rw-r--r--contrib/subtac/subtac_pretyping.ml8
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml62
-rw-r--r--contrib/subtac/subtac_utils.ml6
-rw-r--r--contrib/xml/proof2aproof.ml6
9 files changed, 112 insertions, 112 deletions
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index ebbb5505f6..5b76c95871 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -880,9 +880,9 @@ let interp_pats i isevar env impls pat sign recu =
str "Error parsing pattern: unnexpected left-hand side")
in
isevar := nf_evar_defs !isevar;
- (nf_rel_context_evar (Evd.evars_of !isevar) varsctx,
- nf_env_evar (Evd.evars_of !isevar) env',
- rev_map (nf_evar (Evd.evars_of !isevar)) pats)
+ (nf_rel_context_evar ( !isevar) varsctx,
+ nf_env_evar ( !isevar) env',
+ rev_map (nf_evar ( !isevar)) pats)
let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
@@ -916,8 +916,8 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
let isevar = ref (create_evar_defs Evd.empty) in
let (env', sign), impls = interp_context_evars isevar env l in
let arity = interp_type_evars isevar env' t in
- let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
- let arity = nf_evar (Evd.evars_of !isevar) arity in
+ let sign = nf_rel_context_evar ( !isevar) sign in
+ let arity = nf_evar ( !isevar) arity in
let arity =
if with_comp then
let compid = add_suffix i "_comp" in
@@ -942,11 +942,11 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
Option.iter (Command.declare_interning_data data) nt;
map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
in
- let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
- let arity = nf_evar (Evd.evars_of !isevar) arity in
+ let sign = nf_rel_context_evar ( !isevar) sign in
+ let arity = nf_evar ( !isevar) arity in
let prob = (i, sign, arity) in
- let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in
- let fixdecls = nf_rel_context_evar (Evd.evars_of !isevar) fixdecls in
+ let fixenv = nf_env_evar ( !isevar) fixenv in
+ let fixdecls = nf_rel_context_evar ( !isevar) fixdecls in
(* let ce = check_evars fixenv Evd.empty !isevar in *)
(* List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *)
let is_recursive, env' =
@@ -966,7 +966,7 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
else t, ty
in
let obls, t', ty' =
- Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 ~status t ty
+ Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty
in
if is_recursive then
ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 09ee456d7c..00ed62ac88 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -310,7 +310,7 @@ let unify_tomatch_with_patterns isevars env loc typ pats =
| None -> NotInd (None,typ)
| Some (_,(ind,_)) ->
inh_coerce_to_ind isevars env typ ind;
- try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+ try IsInd (typ,find_rectype env ( !isevars) typ)
with Not_found -> NotInd (None,typ)
let find_tomatch_tycon isevars env loc = function
@@ -324,9 +324,9 @@ let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
let j = typing_fun tycon env tomatch in
let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
isevars := evd;
- let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
+ let typ = nf_evar ( !isevars) j.uj_type in
let t =
- try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+ try IsInd (typ,find_rectype env ( !isevars) typ)
with Not_found ->
unify_tomatch_with_patterns isevars env loc typ pats in
(j.uj_val,t)
@@ -348,7 +348,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
the first pattern type and forget about the others *)
let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in
let typ =
- try IsInd (typ,find_rectype pb.env (Evd.evars_of !(pb.isevars)) typ)
+ try IsInd (typ,find_rectype pb.env ( !(pb.isevars)) typ)
with Not_found -> NotInd (None,typ) in
let tomatch = ((current,typ),deps) in
match typ with
@@ -366,7 +366,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
else
(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
- let sigma = Evd.evars_of !(pb.isevars) in
+ let sigma = !(pb.isevars) in
let typ = IsInd (indt,find_rectype pb.env sigma indt) in
((current,typ),deps))
| _ -> tomatch
@@ -799,7 +799,7 @@ let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k
let reloc_operator (k,n) = function OpRel p when p > k ->
let rec unify_clauses k pv =
- let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (Evd.evars_of isevars)) p) pv in
+ let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) ( isevars)) p) pv in
let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv'
then
@@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf =
(* Empiric normalization: p may depend in a irrelevant way on args of the*)
(* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
let typs =
- Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs
+ Array.map (local_strong whd_beta ( !isevars)) typs
in
let eqns = array_map2 prepare_unif_pb typs cstrs in
(* First strategy: no dependencies at all *)
@@ -846,7 +846,7 @@ let infer_predicate loc env isevars typs cstrs indf =
(true,pred) (* true = dependent -- par défaut *)
else
(*
- let s = get_sort_of env (evars_of isevars) typs.(0) in
+ let s = get_sort_of env ( isevars) typs.(0) in
let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
let caseinfo = make_default_case_info mis in
let brs = array_map2 abstract_conclusion typs cstrs in
@@ -1040,11 +1040,11 @@ let find_predicate loc env isevars p typs cstrs current
(IndType (indf,realargs)) tms =
let (dep,pred) =
match p with
- | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p
+ | Some p -> abstract_predicate env ( !isevars) indf current tms p
| None -> infer_predicate loc env isevars typs cstrs indf in
- let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in
+ let typ = whd_beta ( !isevars) (applist (pred, realargs)) in
if dep then
- (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])),
+ (pred, whd_beta ( !isevars) (applist (typ, [current])),
new_Type ())
else
(pred, typ, new_Type ())
@@ -1271,7 +1271,7 @@ and compile_generalization pb d rest =
and compile_alias pb (deppat,nondeppat,d,t) rest =
let history = simplify_history pb.history in
let sign, newenv, mat =
- insert_aliases pb.env (Evd.evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in
+ insert_aliases pb.env ( !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in
let n = List.length sign in
(* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
@@ -1427,14 +1427,14 @@ let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in
let names = List.rev (List.map (List.map pi1) signs) in
let allargs =
- List.map (fun c -> lift n (nf_betadeltaiota env (Evd.evars_of !isevars) c)) allargs in
+ List.map (fun c -> lift n (nf_betadeltaiota env ( !isevars) c)) allargs in
let rec build_skeleton env c =
(* Don't put into normal form, it has effects on the synthesis of evars *)
- (* let c = whd_betadeltaiota env (evars_of isevars) c in *)
+ (* let c = whd_betadeltaiota env ( isevars) c in *)
(* We turn all subterms possibly dependent into an evar with maximum ctxt*)
if isEvar c or List.exists (eq_constr c) allargs then
e_new_evar isevars env ~src:(loc, Evd.CasesType)
- (Retyping.get_type_of env (Evd.evars_of !isevars) c)
+ (Retyping.get_type_of env ( !isevars) c)
else
map_constr_with_full_binders push_rel build_skeleton env c
in
@@ -1595,7 +1595,7 @@ let constr_of_pat env isevars arsign pat avoid =
PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
| PatCstr (l,((_, i) as cstr),args,alias) ->
let cind = inductive_of_constructor cstr in
- let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in
+ let IndType (indf, _) = find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) in
let ind, params = dest_ind_family indf in
if ind <> cind then error_bad_constructor_loc l cstr ind;
let cstrs = get_constructors env indf in
@@ -1619,8 +1619,8 @@ let constr_of_pat env isevars arsign pat avoid =
let cstr = mkConstruct ci.cs_cstr in
let app = applistc cstr (List.map (lift (List.length sign)) params) in
let app = applistc app args in
- let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in
- let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in
+ let apptype = Retyping.get_type_of env ( !isevars) app in
+ let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in
match alias with
Anonymous ->
pat', sign, app, apptype, realargs, n, avoid
@@ -2047,14 +2047,14 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
(* Build the dependent arity signature, the equalities which makes
the first part of the predicate and their instantiations. *)
let avoid = [] in
- build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign
+ build_dependent_signature env ( !isevars) avoid tomatchs arsign
in
let tycon, arity =
match valcon_of_tycon tycon with
| None -> let ev = mkExistential env isevars in ev, ev
| Some t ->
- t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
+ t, prepare_predicate_from_arsign_tycon loc env ( !isevars)
tomatchs sign (lift tomatchs_len t)
in
let neqs, arity =
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 15729b6266..8ef2153464 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -30,7 +30,7 @@ open Util
module SPretyping = Subtac_pretyping.Pretyping
let interp_binder_evars evdref env na t =
- let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in
+ let t = Constrintern.intern_gen true ( !evdref) env t in
SPretyping.understand_tcc_evars evdref env IsType t
let interp_binders_evars isevars env avoid l =
@@ -65,7 +65,7 @@ let interp_constrs_evars isevars env avoid l =
let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
SPretyping.understand_tcc_evars evdref env kind
- (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
+ (intern_gen (kind=IsType) ~impls ( !evdref) env c)
let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
@@ -94,7 +94,7 @@ let substitution_of_constrs ctx cstrs =
let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) 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 ->
@@ -134,7 +134,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let env' = push_rel_context ctx' env in
isevars := Evarutil.nf_evar_defs !isevars;
isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
- let sigma = Evd.evars_of !isevars in
+ let sigma = !isevars in
let subst = List.map (Evarutil.nf_evar sigma) subst in
let subst =
let props =
@@ -188,7 +188,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
Impargs.declare_manual_implicits false gr ~enriching:false imps;
Typeclasses.add_instance inst
in
- let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+ let evm = Subtac_utils.evars_of_term ( !isevars) Evd.empty term in
let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 0af732f858..54114b0b06 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -83,7 +83,7 @@ module Coercion = struct
| Type _, Prop Null -> Prop Null
| _, Type _ -> s2
- let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
+ let hnf env isevars c = whd_betadeltaiota env ( !isevars) c
let lift_args n sign =
let rec liftrec k = function
@@ -109,7 +109,7 @@ module Coercion = struct
and coerce loc env isevars (x : Term.constr) (y : Term.constr)
: (Term.constr -> Term.constr) option
=
- let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
+ let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in
let rec coerce_unify env x y =
let x = hnf env isevars x and y = hnf env isevars y in
try
@@ -119,7 +119,7 @@ module Coercion = struct
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
let dest_prod c =
- match Reductionops.splay_prod_n env (evars_of !isevars) 1 c with
+ match Reductionops.splay_prod_n env ( !isevars) 1 c with
| [(na,b,t)], c -> (na,t), c
| _ -> raise NoSubtacCoercion
in
@@ -209,7 +209,7 @@ module Coercion = struct
isevars := evs;
let (n, dom, rng) = destLambda t in
let (domk, args) = destEvar dom in
- isevars := evar_define domk a !isevars;
+ isevars := define domk a !isevars;
t, rng
| _ -> raise NoSubtacCoercion
in
@@ -252,7 +252,7 @@ module Coercion = struct
end
else
if i = i' && len = Array.length l' then
- let evm = evars_of !isevars in
+ let evm = !isevars in
(try subco ()
with NoSubtacCoercion ->
let typ = Typing.type_of env evm c in
@@ -264,7 +264,7 @@ module Coercion = struct
subco ()
| x, y when x = y ->
if Array.length l = Array.length l' then
- let evm = evars_of !isevars in
+ let evm = !isevars in
let lam_type = Typing.type_of env evm c in
let lam_type' = Typing.type_of env evm c' in
(* if not (is_arity env evm lam_type) then ( *)
@@ -357,7 +357,7 @@ module Coercion = struct
with _ -> anomaly "apply_coercion"
let inh_app_fun env isevars j =
- let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+ let t = whd_betadeltaiota env ( isevars) j.uj_type in
match kind_of_term t with
| Prod (_,_,_) -> (isevars,j)
| Evar ev when not (is_defined_evar isevars ev) ->
@@ -366,8 +366,8 @@ module Coercion = struct
| _ ->
(try
let t,p =
- lookup_path_to_fun_from env (evars_of isevars) j.uj_type in
- (isevars,apply_coercion env (evars_of isevars) p j t)
+ lookup_path_to_fun_from env ( isevars) j.uj_type in
+ (isevars,apply_coercion env ( isevars) p j t)
with Not_found ->
try
let coercef, t = mu env isevars t in
@@ -377,14 +377,14 @@ module Coercion = struct
let inh_tosort_force loc env isevars j =
try
- let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in
- let j1 = apply_coercion env (evars_of isevars) p j t in
- (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+ let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
+ let j1 = apply_coercion env ( isevars) p j t in
+ (isevars,type_judgment env (j_nf_evar ( isevars) j1))
with Not_found ->
- error_not_a_type_loc loc env (evars_of isevars) j
+ error_not_a_type_loc loc env ( isevars) j
let inh_coerce_to_sort loc env isevars j =
- let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+ let typ = whd_betadeltaiota env ( isevars) j.uj_type in
match kind_of_term typ with
| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
| Evar ev when not (is_defined_evar isevars ev) ->
@@ -394,13 +394,13 @@ module Coercion = struct
inh_tosort_force loc env isevars j
let inh_coerce_to_base loc env isevars j =
- let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+ let typ = whd_betadeltaiota env ( isevars) j.uj_type in
let ct, typ' = mu env isevars typ in
isevars, { uj_val = app_opt ct j.uj_val;
uj_type = typ' }
let inh_coerce_to_prod loc env isevars t =
- let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in
+ let typ = whd_betadeltaiota env ( isevars) (snd t) in
let _, typ' = mu env isevars typ in
isevars, (fst t, typ')
@@ -411,10 +411,10 @@ module Coercion = struct
else
let v', t' =
try
- let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
+ let t2,t1,p = lookup_path_between env ( evd) (t,c1) in
match v with
Some v ->
- let j = apply_coercion env (evars_of evd) p
+ let j = apply_coercion env ( evd) p
{uj_val = v; uj_type = t} t2 in
Some j.uj_val, j.uj_type
| None -> None, t
@@ -430,8 +430,8 @@ module Coercion = struct
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
- kind_of_term (whd_betadeltaiota env (evars_of evd) t),
- kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
+ kind_of_term (whd_betadeltaiota env ( evd) t),
+ kind_of_term (whd_betadeltaiota env ( evd) c1)
with
| Prod (name,t1,t2), Prod (_,u1,u2) ->
(* Conversion did not work, we may succeed with a coercion. *)
@@ -463,7 +463,7 @@ module Coercion = struct
(Some (nf_isevar evd cj.uj_val))
(nf_isevar evd cj.uj_type) (nf_isevar evd t)
with NoCoercion ->
- let sigma = evars_of evd in
+ let sigma = evd in
try
coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
with NoSubtacCoercion ->
@@ -484,7 +484,7 @@ module Coercion = struct
| Some (init, cur) -> init, cur
in
try
- let rels, rng = Reductionops.splay_prod_n env (evars_of isevars) nabs t in
+ let rels, rng = Reductionops.splay_prod_n env ( isevars) nabs t in
(* The final range free variables must have been replaced by evars, we accept only that evars
in rng are applied to free vars. *)
if noccur_with_meta 1 (succ nabs) rng then (
@@ -497,7 +497,7 @@ module Coercion = struct
with NoCoercion ->
coerce_itf loc env' isevars None t t')
with NoSubtacCoercion ->
- let sigma = evars_of isevars in
+ let sigma = isevars in
error_cannot_coerce env' sigma (t, t'))
else isevars
with _ -> isevars
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 4876b06555..674805962d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -57,7 +57,7 @@ let evar_nf isevars c =
let interp_gen kind isevars env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
- let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in
+ let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
evar_nf isevars c'
@@ -75,14 +75,14 @@ let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
let interp_open_constr isevars env c =
msgnl (str "Pretyping " ++ my_print_constr_expr c);
- let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
+ let c = Constrintern.intern_constr ( !isevars) env c in
let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
evar_nf isevars c'
let interp_constr_judgment isevars env c =
let j =
SPretyping.understand_judgment_tcc isevars env
- (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+ (Constrintern.intern_constr ( !isevars) env c)
in
{ uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
@@ -95,11 +95,11 @@ let locate_if_isevar loc na = function
| x -> x
let interp_binder sigma env na t =
- let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
+ let t = Constrintern.intern_gen true ( !sigma) env t in
SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
let interp_context_evars evdref env params =
- let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in
+ let bl = Constrintern.intern_context false ( !evdref) env params in
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
@@ -299,8 +299,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let fullcoqc = Evarutil.nf_isevar !isevars def in
let fullctyp = Evarutil.nf_isevar !isevars typ in
- let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in
- let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
+ let evm =evars_of_term ( !isevars) Evd.empty fullctyp in
+ let evm = evars_of_term ( !isevars) evm fullcoqc in
let evm = non_instanciated_map env isevars evm in
let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
@@ -351,7 +351,7 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
let push_named_context = List.fold_right push_named
let check_evars env initial_sigma evd c =
- let sigma = evars_of evd in
+ let sigma = evd in
let c = nf_evar sigma c in
let rec proc_rec c =
match kind_of_term c with
@@ -374,7 +374,7 @@ let interp_recursive fixkind l boxed =
let fixnames = List.map (fun fix -> fix.Command.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
@@ -397,9 +397,9 @@ let interp_recursive fixkind l boxed =
(* Instantiate evars and check all are resolved *)
let evd,_ = Evarconv.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 rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
+ let fixdefs = List.map (nf_evar ( evd)) fixdefs in
+ let fixtypes = List.map (nf_evar ( evd)) fixtypes in
+ let rec_sign = nf_named_context_evar ( evd) rec_sign in
let recdefs = List.length rec_sign in
List.iter (check_evars env_rec Evd.empty evd) fixdefs;
@@ -410,7 +410,7 @@ let interp_recursive fixkind l boxed =
(* Get the interesting evars, those that were not instanciated *)
let isevars = Evd.undefined_evars evd in
- let evm = Evd.evars_of isevars in
+ let evm = isevars in
(* Solve remaining evars *)
let rec collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 0159de5427..d9df5b34c1 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -74,7 +74,7 @@ let interp env isevars c tycon =
let evd,_ = consider_remaining_unif_problems env !isevars in
(* let unevd = undefined_evars evd in *)
let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
- let evm = evars_of unevd' in
+ let evm = unevd' in
isevars := unevd';
nf_evar evm j.uj_val, nf_evar evm j.uj_type
@@ -86,8 +86,8 @@ let find_with_index x l =
open Vernacexpr
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type ( evd) env
let env_with_binders env isevars l =
let rec aux ((env, rels) as acc) = function
@@ -123,7 +123,7 @@ let subtac_process env isevars id bl c tycon =
let c = coqintern_constr !isevars env c in
let imps = Implicit_quantifiers.implicits_of_rawterm c in
let coqc, ctyp = interp env isevars c tycon in
- let evm = non_instanciated_map env isevars (evars_of !isevars) in
+ let evm = non_instanciated_map env isevars ( !isevars) in
let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
evm, coqc, ty, imps
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 023213ecbc..01fe4ef6f1 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -79,14 +79,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
for i = 0 to lt-1 do
if not (e_cumul env isevars (vdefj.(i)).uj_type
(lift lt lar.(i))) then
- error_ill_typed_rec_body_loc loc env (evars_of !isevars)
+ error_ill_typed_rec_body_loc loc env ( !isevars)
i lna vdefj lar
done
let check_branches_message loc env isevars c (explft,lft) =
for i = 0 to Array.length explft - 1 do
if not (e_cumul env isevars lft.(i) explft.(i)) then
- let sigma = evars_of !isevars in
+ let sigma = !isevars in
error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
done
@@ -99,7 +99,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(*
let evar_type_case isevars env ct pt lft p c =
- let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
+ let (mind,bty,rslty) = type_case_branches env ( isevars) ct pt p c
in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
*)
@@ -158,7 +158,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RType _ -> judge_of_new_Type ()
(* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
- (* in environment [env], with existential variables [(evars_of isevars)] and *)
+ (* in environment [env], with existential variables [( isevars)] and *)
(* the type constraint tycon *)
let rec pretype (tycon : type_constraint) env isevars lvar c =
(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
@@ -179,12 +179,12 @@ module SubtacPretyping_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.find (evars_of !isevars) ev) in
+ let hyps = evar_context (Evd.find ( !isevars) ev) in
let args = match instopt with
| None -> instance_from_named_context hyps
| Some inst -> failwith "Evar subtitutions not implemented" in
let c = mkEvar (ev, args) in
- let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+ let j = (Retyping.get_judgment_of env ( !isevars) c) in
inh_conv_coerce_to_tycon loc env isevars j tycon
| RPatVar (loc,(someta,n)) ->
@@ -246,8 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
evar_type_fixpoint loc env isevars names ftys vdefj;
- let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in
- let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in
+ let ftys = Array.map (nf_evar ( !isevars)) ftys in
+ let fdefs = Array.map (fun x -> nf_evar ( !isevars) (j_val x)) vdefj in
let fixj = match fixkind with
| RFix (vn,i) ->
(* First, let's find the guard indexes. *)
@@ -297,7 +297,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| c::rest ->
let argloc = loc_of_rawconstr c in
let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
- let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
+ let resty = whd_betadeltaiota env ( !isevars) resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
Option.iter (fun ty -> isevars :=
@@ -315,14 +315,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ ->
let hj = pretype empty_tycon env isevars lvar c in
error_cant_apply_not_functional_loc
- (join_loc floc argloc) env (evars_of !isevars)
+ (join_loc floc argloc) env ( !isevars)
resj [hj]
in
- let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
+ let resj = j_nf_evar ( !isevars) (apply_rec env 1 fj ftycon args) in
let resj =
match kind_of_term resj.uj_val with
| App (f,args) when isInd f or isConst f ->
- let sigma = evars_of !isevars in
+ let sigma = !isevars in
let c = mkApp (f,Array.map (whd_evar sigma) args) in
let t = Retyping.get_type_of env sigma c in
make_judge c t
@@ -369,10 +369,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RLetTuple (loc,nal,(na,po),c,d) ->
let cj = pretype empty_tycon env isevars lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env (evars_of !isevars) cj.uj_type
+ try find_rectype env ( !isevars) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env (evars_of !isevars) cj
+ error_case_not_inductive_loc cloc env ( !isevars) cj
in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 1 then
@@ -396,14 +396,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| Some p ->
let env_p = push_rels psign env in
let pj = pretype_type empty_valcon env_p isevars lvar p in
- let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+ let ccl = nf_evar ( !isevars) pj.utj_val in
let psign = make_arity_signature env true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
let inst =
(Array.to_list cs.cs_concl_realargs)
@[build_dependent_constructor cs] in
let lp = lift cs.cs_nargs p in
- let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
+ let fty = hnf_lam_applist env ( !isevars) lp inst in
let fj = pretype (mk_tycon fty) env_f isevars lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let v =
@@ -416,12 +416,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f isevars lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
- let ccl = nf_evar (evars_of !isevars) fj.uj_type in
+ let ccl = nf_evar ( !isevars) fj.uj_type in
let ccl =
if noccur_between 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl
else
- error_cant_find_case_type_loc loc env (evars_of !isevars)
+ error_cant_find_case_type_loc loc env ( !isevars)
cj.uj_val in
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
@@ -434,10 +434,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env isevars lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env (evars_of !isevars) cj.uj_type
+ try find_rectype env ( !isevars) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
+ error_case_not_inductive_loc cloc env ( !isevars) cj in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 2 then
user_err_loc (loc,"",
@@ -456,7 +456,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| Some p ->
let env_p = push_rels psign env in
let pj = pretype_type empty_valcon env_p isevars lvar p in
- let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+ let ccl = nf_evar ( !isevars) pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred;
@@ -470,8 +470,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
- let pred = nf_evar (evars_of !isevars) pred in
- let p = nf_evar (evars_of !isevars) p in
+ let pred = nf_evar ( !isevars) pred in
+ let p = nf_evar ( !isevars) p in
(* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
let f cs b =
let n = rel_context_length cs.cs_args in
@@ -525,7 +525,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RDynamic (loc,d) ->
if (tag d) = "constr" then
let c = constr_out d in
- let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+ let j = (Retyping.get_judgment_of env ( !isevars) c) in
j
(*inh_conv_coerce_to_tycon loc env isevars j tycon*)
else
@@ -537,7 +537,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(match valcon with
| Some v ->
let s =
- let sigma = evars_of !isevars in
+ let sigma = !isevars in
let t = Retyping.get_type_of env sigma v in
match kind_of_term (whd_betadeltaiota env sigma t) with
| Sort s -> s
@@ -561,7 +561,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
if e_cumul env isevars v tj.utj_val then tj
else
error_unexpected_type_loc
- (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
+ (loc_of_rawconstr c) env ( !isevars) tj.utj_val v
let pretype_gen_aux isevars env lvar kind c =
let c' = match kind with
@@ -572,12 +572,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(pretype_type empty_valcon env isevars lvar c).utj_val in
let evd,_ = consider_remaining_unif_problems env !isevars in
isevars:=evd;
- nf_evar (evars_of !isevars) c'
+ nf_evar ( !isevars) c'
let pretype_gen isevars env lvar kind c =
let c = pretype_gen_aux isevars env lvar kind c in
isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars;
- nf_evar (evars_of !isevars) c
+ nf_evar ( !isevars) c
(* TODO: comment faire remonter l'information si le typage a resolu des
variables du sigma original. il faudrait que la fonction de typage
@@ -587,14 +587,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let understand_judgment sigma env c =
let isevars = ref (create_evar_defs sigma) in
let j = pretype empty_tycon env isevars ([],[]) c in
- let j = j_nf_evar (evars_of !isevars) j in
+ let j = j_nf_evar ( !isevars) j in
let isevars,_ = consider_remaining_unif_problems env !isevars in
check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
j
let understand_judgment_tcc isevars env c =
let j = pretype empty_tycon env isevars ([],[]) c in
- let sigma = evars_of !isevars in
+ let sigma = !isevars in
let j = j_nf_evar sigma j in
j
@@ -635,7 +635,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in
!isevars, c
in
- Evd.evars_of ev, t
+ ev, t
end
module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index cdbc402321..ba30ee1900 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -437,7 +437,7 @@ let pr_evar_info evi =
in
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
-let pr_evar_map sigma =
+let pr_evar_defs sigma =
h 0
(prlist_with_sep pr_fnl
(fun (ev,evi) ->
@@ -455,9 +455,9 @@ let pr_constraints pbs =
let pr_evar_defs evd =
let pp_evm =
- let evars = evars_of evd in
+ let evars = evd in
if evars = empty then mt() else
- str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
+ str"EVARS:"++brk(0,1)++pr_evar_defs evars++fnl() in
let pp_met =
if meta_list evd = [] then mt() else
str"METAS:"++brk(0,1)++pr_meta_map evd in
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 30dc7b710e..f7524671fd 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -149,7 +149,7 @@ let extract_open_proof sigma pf =
in
let unsharedconstr =
let evar_nf_constr =
- nf_evar (Evd.evars_of !evd)
+ nf_evar ( !evd)
~preserve:(function e -> S.mem e !unshared_constrs) constr
in
Unshare.unshare
@@ -159,14 +159,14 @@ let extract_open_proof sigma pf =
(*CSC: debugging stuff to be removed *)
if ProofTreeHash.mem proof_tree_to_constr node then
Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ")
- (Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ;
+ (Tactic_printer.print_proof ( !evd) [] node)) ;
ProofTreeHash.add proof_tree_to_constr node unsharedconstr ;
unshared_constrs := S.add unsharedconstr !unshared_constrs ;
unsharedconstr
in
let unshared_pf = unshare_proof_tree pf in
let pfterm = proof_extractor [] unshared_pf in
- (pfterm, Evd.evars_of !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
+ (pfterm, !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
unshared_pf)
;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-12 07:17:48 +0000