aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml16
-rw-r--r--pretyping/cases.mli2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/evarutil.ml28
-rw-r--r--pretyping/evarutil.mli12
-rw-r--r--pretyping/pretyping.ml46
-rw-r--r--pretyping/pretyping.mli14
-rw-r--r--pretyping/tacred.ml66
-rw-r--r--pretyping/unification.ml6
11 files changed, 98 insertions, 98 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 62bfef886..d52f410d2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -277,7 +277,7 @@ let inductive_template evdref env tmloc ind =
match b with
| None ->
let ty' = substl subst ty in
- let e = e_new_evar evdref env ~src:(hole_source n) ty' in
+ let e = e_new_evar env evdref ~src:(hole_source n) ty' in
(e::subst,e::evarl,n+1)
| Some b ->
(substl subst b::subst,evarl,n+1))
@@ -352,7 +352,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
(* Utils *)
let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref =
- let e, u = e_new_type_evar evdref univ_flexible_alg env ~src:src in e
+ let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e
let evd_comb2 f evdref x y =
let (evd',y) = f !evdref x y in
@@ -1574,7 +1574,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
(fun i _ ->
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
1 (rel_context env) in
- let ev = e_new_evar evdref env ~src:(loc, Evar_kinds.CasesType) ty in
+ let ev = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in
evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref;
ev
| _ ->
@@ -1603,7 +1603,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
let filter = Filter.make (rel_filter @ named_filter) in
let candidates = u :: List.map mkRel vl in
let ev =
- e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType)
+ e_new_evar extenv evdref ~src:(loc, Evar_kinds.CasesType)
~filter ~candidates ty in
lift k ev
in
@@ -1617,7 +1617,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
let n = rel_context_length (rel_context env) in
let n' = rel_context_length (rel_context tycon_env) in
let impossible_case_type, u =
- e_new_type_evar evdref univ_flexible_alg env ~src:(loc,Evar_kinds.ImpossibleCase) in
+ e_new_type_evar env evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in
(lift (n'-n) impossible_case_type, mkSort u)
| Some t ->
let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
@@ -1858,7 +1858,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
* tycon to make the predicate if it is not closed.
*)
-let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
+let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let preds =
match pred, tycon with
(* No type annotation *)
@@ -1878,7 +1878,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
| Some t -> sigma,t
| None ->
let sigma, (t, _) =
- new_type_evar univ_flexible_alg sigma env ~src:(loc, Evar_kinds.CasesType) in
+ new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType) in
sigma, t
in
(* First strategy: we build an "inversion" predicate *)
@@ -2439,7 +2439,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
with the type of arguments to match; if none is provided, we
build alternative possible predicates *)
let arsign = extract_arity_signature env tomatchs tomatchl in
- let preds = prepare_predicate loc typing_fun !evdref env tomatchs arsign tycon predopt in
+ let preds = prepare_predicate loc typing_fun env !evdref tomatchs arsign tycon predopt in
let compile_for_one_predicate (sigma,nal,pred) =
(* We push the initial terms to match and push their alias to rhs' envs *)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index e51055cef..3ff1d8659 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -114,8 +114,8 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
val prepare_predicate : Loc.t ->
(Evarutil.type_constraint ->
Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
- Evd.evar_map ->
Environ.env ->
+ Evd.evar_map ->
(Term.types * tomatch_type) list ->
Context.rel_context list ->
Constr.constr option ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index dfaff327a..a1279c1f2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -81,7 +81,7 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
open Program
let make_existential loc ?(opaque = Evar_kinds.Define true) env evdref c =
- Evarutil.e_new_evar evdref env ~src:(loc, Evar_kinds.QuestionMark opaque) c
+ Evarutil.e_new_evar env evdref ~src:(loc, Evar_kinds.QuestionMark opaque) c
let app_opt env evdref f t =
whd_betaiota !evdref (app_opt f t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 190a025ac..d125a799b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -763,7 +763,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
(i,t2::ks, m-1, test)
else
let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
- let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
+ let (i',ev) = new_evar env i ~src:dloc (substl ks b) in
(i', ev :: ks, m - 1,test))
(evd,[],List.length bs - 1,fun i -> Success i) bs
in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f5de8c90..631438ddf 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1150,7 +1150,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
else
let evd, k = Evd.new_sort_variable univ_flexible_alg evd in
let evd, ev3 =
- Evarutil.new_pure_evar evd (Evd.evar_hyps evi)
+ Evarutil.new_pure_evar (Evd.evar_hyps evi) evd
~src:evi.evar_source ~filter:evi.evar_filter
?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx)
in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 306032ed9..ddc1ece96 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -351,7 +351,7 @@ let new_pure_evar_full evd evi =
let evd = Evd.add evd evk evi in
(evd, evk)
-let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates ?store typ =
+let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store typ =
let newevk = new_untyped_evar() in
let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in
(evd,newevk)
@@ -359,12 +359,12 @@ let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates ?store typ
let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance =
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
- let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates ?store typ in
+ let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store typ in
(evd,mkEvar (newevk,Array.of_list instance))
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
-let new_evar evd env ?src ?filter ?candidates ?store typ =
+let new_evar env evd ?src ?filter ?candidates ?store typ =
let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
let instance =
@@ -373,13 +373,13 @@ let new_evar evd env ?src ?filter ?candidates ?store typ =
| Some filter -> Filter.filter_list filter instance in
new_evar_instance sign evd typ' ?src ?filter ?candidates ?store instance
-let new_type_evar ?src ?filter rigid evd env =
+let new_type_evar env evd ?src ?filter rigid =
let evd', s = new_sort_variable rigid evd in
- let evd', e = new_evar evd' env ?src ?filter (mkSort s) in
+ let evd', e = new_evar env evd' ?src ?filter (mkSort s) in
evd', (e, s)
-let e_new_type_evar evdref ?src ?filter rigid env =
- let evd', c = new_type_evar ?src ?filter rigid !evdref env in
+let e_new_type_evar env evdref ?src ?filter rigid =
+ let evd', c = new_type_evar env !evdref ?src ?filter rigid in
evdref := evd';
c
@@ -392,8 +392,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
evdref := evd'; mkSort s
(* The same using side-effect *)
-let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ?store ty =
- let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ?store ty in
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ty =
+ let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ty in
evdref := evd';
ev
@@ -482,7 +482,7 @@ let rec check_and_clear_in_constr evdref err ids c =
if Id.Map.is_empty rids then c
else
let env = Context.fold_named_context push_named nhyps ~init:(empty_env) in
- let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
+ let ev'= e_new_evar env evdref ~src:(evar_source evk !evdref) nconcl in
evdref := Evd.define evk ev' !evdref;
let (evk',_) = destEvar ev' in
(* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
@@ -704,17 +704,17 @@ let define_pure_evar_as_product evd evk =
let evenv = evar_env evi in
let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
let s = destSort evi.evar_concl in
- let evd1,(dom,u1) = new_type_evar univ_flexible_alg evd evenv ~filter:(evar_filter evi) in
+ let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
let evd2,rng =
let newenv = push_named (id, None, dom) evenv in
let src = evar_source evk evd1 in
let filter = Filter.extend 1 (evar_filter evi) in
if is_prop_sort s then
(* Impredicative product, conclusion must fall in [Prop]. *)
- new_evar evd1 newenv evi.evar_concl ~src ~filter
+ new_evar newenv evd1 evi.evar_concl ~src ~filter
else
let evd3, (rng, srng) =
- new_type_evar univ_flexible_alg evd1 newenv ~src ~filter in
+ new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
let evd3 = Evd.set_leq_sort evd3 (Type prods) s in
evd3, rng
@@ -757,7 +757,7 @@ let define_pure_evar_as_lambda env evd evk =
let newenv = push_named (id, None, dom) evenv in
let filter = Filter.extend 1 (evar_filter evi) in
let src = evar_source evk evd1 in
- let evd2,body = new_evar evd1 newenv ~src (subst1 (mkVar id) rng) ~filter in
+ let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
let lam = mkLambda (Name id, dom, subst_var id body) in
Evd.define evk lam evd2, lam
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 2d3dd33a3..081c41560 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -22,28 +22,28 @@ val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
val new_evar :
- evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr
val new_pure_evar :
- evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar
val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
(** the same with side-effects *)
val e_new_evar :
- evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t -> types -> constr
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
- ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> evar_map -> env ->
+ env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid ->
evar_map * (constr * sorts)
-val e_new_type_evar : evar_map ref ->
- ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> env -> constr * sorts
+val e_new_type_evar : env -> evar_map ref ->
+ ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> constr * sorts
val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a21548d57..0115f67d5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -364,9 +364,9 @@ let pretype_sort evdref = function
| GSet -> judge_of_set
| GType s -> evd_comb1 judge_of_Type evdref s
-let new_type_evar evdref env loc =
+let new_type_evar env evdref loc =
let e, s =
- evd_comb0 (fun evd -> Evarutil.new_type_evar univ_flexible_alg evd env ~src:(loc,Evar_kinds.InternalHole)) evdref
+ evd_comb0 (fun evd -> Evarutil.new_type_evar env evd univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
in e
let get_projection env cst =
@@ -426,24 +426,24 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let ty =
match tycon with
| Some ty -> ty
- | None -> new_type_evar evdref env loc in
+ | None -> new_type_evar env evdref loc in
let k = Evar_kinds.MatchingVar (someta,n) in
- { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+ { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (loc, k, None) ->
let ty =
match tycon with
| Some ty -> ty
| None ->
- new_type_evar evdref env loc in
- { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+ new_type_evar env evdref loc in
+ { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (loc, k, Some arg) ->
let ty =
match tycon with
| Some ty -> ty
| None ->
- new_type_evar evdref env loc in
+ new_type_evar env evdref loc in
let ist = lvar.ltac_genargs in
let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in
let () = evdref := sigma in
@@ -543,7 +543,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let ctx = smash_rel_context (Inductiveops.inductive_paramdecls ind) in
List.fold_right (fun (n, b, ty) (* par *)args ->
let ty = substl args ty in
- let ev = e_new_evar evdref env ~src:(loc,k) ty in
+ let ev = e_new_evar env evdref ~src:(loc,k) ty in
ev :: args) ctx []
in (ind, List.rev args)
in
@@ -830,7 +830,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
| None ->
let p = match tycon with
| Some ty -> ty
- | None -> new_type_evar evdref env loc
+ | None -> new_type_evar env evdref loc
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar !evdref pred in
@@ -929,7 +929,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function
utj_type = s }
| None ->
let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
- { utj_val = e_new_evar evdref env ~src:(loc, knd) (mkSort s);
+ { utj_val = e_new_evar env evdref ~src:(loc, knd) (mkSort s);
utj_type = s})
| c ->
let j = pretype resolve_tc empty_tycon env evdref lvar c in
@@ -943,7 +943,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function
error_unexpected_type_loc
(loc_of_glob_constr c) env !evdref tj.utj_val v
-let ise_pretype_gen flags sigma env lvar kind c =
+let ise_pretype_gen flags env sigma lvar kind c =
let evdref = ref sigma in
let c' = match kind with
| WithoutTypeConstraint ->
@@ -984,7 +984,7 @@ let on_judgment f j =
let (c,_,t) = destCast (f c) in
{uj_val = c; uj_type = t}
-let understand_judgment sigma env c =
+let understand_judgment env sigma c =
let evdref = ref sigma in
let j = pretype true empty_tycon env evdref empty_lvar c in
let j = on_judgment (fun c ->
@@ -992,14 +992,14 @@ let understand_judgment sigma env c =
evdref := evd; c) j
in j, Evd.evar_universe_context !evdref
-let understand_judgment_tcc evdref env c =
+let understand_judgment_tcc env evdref c =
let j = pretype true empty_tycon env evdref empty_lvar c in
on_judgment (fun c ->
let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
evdref := evd; c) j
-let ise_pretype_gen_ctx flags sigma env lvar kind c =
- let evd, c = ise_pretype_gen flags sigma env lvar kind c in
+let ise_pretype_gen_ctx flags env sigma lvar kind c =
+ let evd, c = ise_pretype_gen flags env sigma lvar kind c in
let evd, f = Evarutil.nf_evars_and_universes evd in
f c, Evd.evar_universe_context evd
@@ -1008,16 +1008,16 @@ let ise_pretype_gen_ctx flags sigma env lvar kind c =
let understand
?(flags=all_and_fail_flags)
?(expected_type=WithoutTypeConstraint)
- sigma env c =
- ise_pretype_gen_ctx flags sigma env empty_lvar expected_type c
+ env sigma c =
+ ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c
-let understand_tcc ?(flags=all_no_fail_flags) sigma env ?(expected_type=WithoutTypeConstraint) c =
- ise_pretype_gen flags sigma env empty_lvar expected_type c
+let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
+ ise_pretype_gen flags env sigma empty_lvar expected_type c
-let understand_tcc_evars ?(flags=all_no_fail_flags) evdref env ?(expected_type=WithoutTypeConstraint) c =
- let sigma, c = ise_pretype_gen flags !evdref env empty_lvar expected_type c in
+let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c =
+ let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in
evdref := sigma;
c
-let understand_ltac flags sigma env lvar kind c =
- ise_pretype_gen flags sigma env lvar kind c
+let understand_ltac flags env sigma lvar kind c =
+ ise_pretype_gen flags env sigma lvar kind c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 695b2b51f..5df4c8372 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -70,10 +70,10 @@ val allow_anonymous_refs : bool ref
unresolved holes as evars and returning the typing contexts of
these evars. Work as [understand_gen] for the rest. *)
-val understand_tcc : ?flags:inference_flags -> evar_map -> env ->
+val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
?expected_type:typing_constraint -> glob_constr -> open_constr
-val understand_tcc_evars : ?flags:inference_flags -> evar_map ref -> env ->
+val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
?expected_type:typing_constraint -> glob_constr -> constr
(** More general entry point with evars from ltac *)
@@ -89,21 +89,21 @@ val understand_tcc_evars : ?flags:inference_flags -> evar_map ref -> env ->
*)
val understand_ltac : inference_flags ->
- evar_map -> env -> ltac_var_map ->
+ env -> evar_map -> ltac_var_map ->
typing_constraint -> glob_constr -> pure_open_constr
(** Standard call to get a constr from a glob_constr, resolving implicit args *)
val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
- evar_map -> env -> glob_constr -> constr Evd.in_evar_universe_context
+ env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
(** Idem but returns the judgment of the understood term *)
-val understand_judgment : evar_map -> env ->
+val understand_judgment : env -> evar_map ->
glob_constr -> unsafe_judgment Evd.in_evar_universe_context
(** Idem but do not fail on unresolved evars *)
-val understand_judgment_tcc : evar_map ref -> env ->
+val understand_judgment_tcc : env -> evar_map ref ->
glob_constr -> unsafe_judgment
(** Trying to solve remaining evars and remaining conversion problems
@@ -128,7 +128,7 @@ val pretype_type :
ltac_var_map -> glob_constr -> unsafe_type_judgment
val ise_pretype_gen :
- inference_flags -> evar_map -> env ->
+ inference_flags -> env -> evar_map ->
ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr
(**/**)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 91447573f..acae69b68 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -104,7 +104,7 @@ let destEvalRefU c = match kind_of_term c with
| Evar ev -> (EvalEvar ev, Univ.Instance.empty)
| _ -> anomaly (Pp.str "Not an unfoldable reference")
-let unsafe_reference_opt_value sigma env eval =
+let unsafe_reference_opt_value env sigma eval =
match eval with
| EvalConst cst ->
(match (lookup_constant cst env).Declarations.const_body with
@@ -118,7 +118,7 @@ let unsafe_reference_opt_value sigma env eval =
Option.map (lift n) v
| EvalEvar ev -> Evd.existential_opt_value sigma ev
-let reference_opt_value sigma env eval u =
+let reference_opt_value env sigma eval u =
match eval with
| EvalConst cst -> constant_opt_value_in env (cst,u)
| EvalVar id ->
@@ -130,8 +130,8 @@ let reference_opt_value sigma env eval u =
| EvalEvar ev -> Evd.existential_opt_value sigma ev
exception NotEvaluable
-let reference_value sigma env c u =
- match reference_opt_value sigma env c u with
+let reference_value env sigma c u =
+ match reference_opt_value env sigma c u with
| None -> raise NotEvaluable
| Some d -> d
@@ -235,7 +235,7 @@ let invert_name labs l na0 env sigma ref = function
match refi with
| None -> None
| Some ref ->
- try match unsafe_reference_opt_value sigma env ref with
+ try match unsafe_reference_opt_value env sigma ref with
| None -> None
| Some c ->
let labs',ccl = decompose_lam c in
@@ -253,7 +253,7 @@ let invert_name labs l na0 env sigma ref = function
[compute_consteval_mutual_fix] only one by one, until finding the
last one before the Fix if the latter is mutually defined *)
-let compute_consteval_direct sigma env ref =
+let compute_consteval_direct env sigma ref =
let rec srec env n labs onlyproj c =
let c',l = whd_betadelta_stack env sigma c in
match kind_of_term c' with
@@ -267,11 +267,11 @@ let compute_consteval_direct sigma env ref =
| Proj (p, d) when isRel d -> EliminationProj n
| _ -> NotAnElimination
in
- match unsafe_reference_opt_value sigma env ref with
+ match unsafe_reference_opt_value env sigma ref with
| None -> NotAnElimination
| Some c -> srec env 0 [] false c
-let compute_consteval_mutual_fix sigma env ref =
+let compute_consteval_mutual_fix env sigma ref =
let rec srec env minarg labs ref c =
let c',l = whd_betalet_stack sigma c in
let nargs = List.length l in
@@ -280,7 +280,7 @@ let compute_consteval_mutual_fix sigma env ref =
srec (push_rel (na,None,t) env) (minarg+1) (t::labs) ref g
| Fix ((lv,i),(names,_,_)) ->
(* Last known constant wrapping Fix is ref = [labs](Fix l) *)
- (match compute_consteval_direct sigma env ref with
+ (match compute_consteval_direct env sigma ref with
| NotAnElimination -> (*Above const was eliminable but this not!*)
NotAnElimination
| EliminationFix (minarg',minfxargs,infos) ->
@@ -293,31 +293,31 @@ let compute_consteval_mutual_fix sigma env ref =
| _ when isEvalRef env c' ->
(* Forget all \'s and args and do as if we had started with c' *)
let ref,_ = destEvalRefU c' in
- (match unsafe_reference_opt_value sigma env ref with
+ (match unsafe_reference_opt_value env sigma ref with
| None -> anomaly (Pp.str "Should have been trapped by compute_direct")
| Some c -> srec env (minarg-nargs) [] ref c)
| _ -> (* Should not occur *) NotAnElimination
in
- match unsafe_reference_opt_value sigma env ref with
+ match unsafe_reference_opt_value env sigma ref with
| None -> (* Should not occur *) NotAnElimination
| Some c -> srec env 0 [] ref c
-let compute_consteval sigma env ref =
- match compute_consteval_direct sigma env ref with
+let compute_consteval env sigma ref =
+ match compute_consteval_direct env sigma ref with
| EliminationFix (_,_,(nbfix,_,_)) when not (Int.equal nbfix 1) ->
- compute_consteval_mutual_fix sigma env ref
+ compute_consteval_mutual_fix env sigma ref
| elim -> elim
-let reference_eval sigma env = function
+let reference_eval env sigma = function
| EvalConst cst as ref ->
(try
Cmap.find cst !eval_table
with Not_found -> begin
- let v = compute_consteval sigma env ref in
+ let v = compute_consteval env sigma ref in
eval_table := Cmap.add cst v !eval_table;
v
end)
- | ref -> compute_consteval sigma env ref
+ | ref -> compute_consteval env sigma ref
(* If f is bound to EliminationFix (n',infos), then n' is the minimal
number of args for starting the reduction and infos is
@@ -385,7 +385,7 @@ let substl_with_function subst sigma constr =
if i <= k + Array.length v then
match v.(i-k-1) with
| (fx, Some (min, ref)) ->
- let (sigma, evk) = Evarutil.new_pure_evar !evd venv dummy in
+ let (sigma, evk) = Evarutil.new_pure_evar venv !evd dummy in
evd := sigma;
minargs := Evar.Map.add evk min !minargs;
lift k (mkEvar (evk, [|fx;ref|]))
@@ -415,7 +415,7 @@ let solve_arity_problem env sigma fxminargs c =
List.iter (check strict) rcargs
| (Var _|Const _) when isEvalRef env h ->
(let ev, u = destEvalRefU h in
- match reference_opt_value sigma env ev u with
+ match reference_opt_value env sigma ev u with
| Some h' ->
let bak = !evm in
(try List.iter (check false) rcargs
@@ -529,7 +529,7 @@ let match_eval_ref env constr =
| Evar ev -> Some (EvalEvar ev, Univ.Instance.empty)
| _ -> None
-let match_eval_ref_value sigma env constr =
+let match_eval_ref_value env sigma constr =
match kind_of_term constr with
| Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
Some (constant_value_in env (sp, u))
@@ -545,7 +545,7 @@ let special_red_case env sigma whfun (ci, p, c, lf) =
let (constr, cargs) = whfun s in
match match_eval_ref env constr with
| Some (ref, u) ->
- (match reference_opt_value sigma env ref u with
+ (match reference_opt_value env sigma ref u with
| None -> raise Redelimination
| Some gvalue ->
if reducible_mind_case gvalue then
@@ -657,20 +657,20 @@ let rec red_elim_const env sigma ref u largs =
n >= 0 && not is_empty && nargs >= n,
List.mem `ReductionDontExposeCase f
in
- try match reference_eval sigma env ref with
+ try match reference_eval env sigma ref with
| EliminationCases n when nargs >= n ->
- let c = reference_value sigma env ref u in
+ let c = reference_value env sigma ref u in
let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
let whfun = whd_simpl_stack env sigma in
(special_red_case env sigma whfun (destCase c'), lrest), nocase
| EliminationProj n when nargs >= n ->
- let c = reference_value sigma env ref u in
+ let c = reference_value env sigma ref u in
let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
let whfun = whd_construct_stack env sigma in
let whfun' = whd_simpl_stack env sigma in
(reduce_proj env sigma whfun whfun' c', lrest), nocase
| EliminationFix (min,minfxargs,infos) when nargs >= min ->
- let c = reference_value sigma env ref u in
+ let c = reference_value env sigma ref u in
let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) u largs in
let whfun = whd_construct_stack env sigma in
@@ -679,7 +679,7 @@ let rec red_elim_const env sigma ref u largs =
| Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
| EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
let rec descend (ref,u) args =
- let c = reference_value sigma env ref u in
+ let c = reference_value env sigma ref u in
if evaluable_reference_eq ref refgoal then
(c,args)
else
@@ -693,11 +693,11 @@ let rec red_elim_const env sigma ref u largs =
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
| NotAnElimination when unfold_nonelim ->
- let c = reference_value sigma env ref u in
+ let c = reference_value env sigma ref u in
(whd_betaiotazeta sigma (applist (c, largs)), []), nocase
| _ -> raise Redelimination
with Redelimination when unfold_anyway ->
- let c = reference_value sigma env ref u in
+ let c = reference_value env sigma ref u in
(whd_betaiotazeta sigma (applist (c, largs)), []), nocase
and reduce_params env sigma stack l =
@@ -786,7 +786,7 @@ and whd_construct_stack env sigma s =
if reducible_mind_case constr then s'
else match match_eval_ref env constr with
| Some (ref, u) ->
- (match reference_opt_value sigma env ref u with
+ (match reference_opt_value env sigma ref u with
| None -> raise Redelimination
| Some gvalue -> whd_construct_stack env sigma (applist(gvalue, cargs)))
| _ -> raise Redelimination
@@ -839,7 +839,7 @@ let try_red_product env sigma c =
| Some (ref, u) ->
(* TO DO: re-fold fixpoints after expansion *)
(* to get true one-step reductions *)
- (match reference_opt_value sigma env ref u with
+ (match reference_opt_value env sigma ref u with
| None -> raise Redelimination
| Some c -> c)
| _ -> raise Redelimination)
@@ -893,7 +893,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
(try
redrec (red_elim_const env sigma ref stack)
with Redelimination ->
- match reference_opt_value sigma env ref with
+ match reference_opt_value env sigma ref with
| Some c ->
(match kind_of_term (strip_lam c) with
| CoFix _ | Fix _ -> s
@@ -916,7 +916,7 @@ let whd_simpl_stack =
let whd_simpl_orelse_delta_but_fix env sigma c =
let rec redrec s =
let (constr, stack as s') = whd_simpl_stack env sigma s in
- match match_eval_ref_value sigma env constr with
+ match match_eval_ref_value env sigma constr with
| Some c ->
(match kind_of_term (strip_lam c) with
| CoFix _ | Fix _ -> s'
@@ -1188,7 +1188,7 @@ let one_step_reduce env sigma c =
(try
fst (red_elim_const env sigma ref u stack)
with Redelimination ->
- match reference_opt_value sigma env ref u with
+ match reference_opt_value env sigma ref u with
| Some d -> (d, stack)
| None -> raise NotStepReducible)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 63c30eb35..124faf05b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -86,7 +86,7 @@ let set_occurrences_of_last_arg args =
Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
let abstract_list_all_with_dependencies env evd typ c l =
- let evd,ev = new_evar evd env typ in
+ let evd,ev = new_evar env evd typ in
let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in
let argoccs = set_occurrences_of_last_arg (snd ev') in
let evd,b =
@@ -135,7 +135,7 @@ let pose_all_metas_as_evars env evd t =
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
let src = Evd.evar_source_of_meta mv !evdref in
- let ev = Evarutil.e_new_evar evdref env ~src ty in
+ let ev = Evarutil.e_new_evar env evdref ~src ty in
evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
ev)
| _ ->
@@ -982,7 +982,7 @@ let applyHead env evd n c =
match kind_of_term (whd_betadeltaiota env evd cty) with
| Prod (_,c1,c2) ->
let (evd',evar) =
- Evarutil.new_evar evd env ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
+ Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
| _ -> error "Apply_Head_Then"
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 02:28:44 +0000