aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml2
-rw-r--r--plugins/subtac/subtac_classes.ml2
-rw-r--r--plugins/subtac/subtac_coercion.ml8
-rw-r--r--plugins/subtac/subtac_command.ml2
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml42
-rw-r--r--pretyping/coercion.ml14
-rw-r--r--tactics/rewrite.ml42
7 files changed, 36 insertions, 36 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c651d11cb..18fd16279 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1515,7 +1515,7 @@ let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
- let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in
+ let c = intern_gen (kind=IsType) ~impls !evdref env c in
Default.understand_tcc_evars evdref env kind c
let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index fccb2f933..88f88b7f2 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -28,7 +28,7 @@ module SPretyping = Subtac_pretyping.Pretyping
let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
SPretyping.understand_tcc_evars evdref env kind
- (intern_gen (kind=IsType) ~impls ( !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
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index d09ab4312..a1159dcaa 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -408,10 +408,10 @@ module Coercion = struct
else
let v', t' =
try
- let t2,t1,p = lookup_path_between env ( 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 ( 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
@@ -427,8 +427,8 @@ module Coercion = struct
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
- kind_of_term (whd_betadeltaiota env ( evd) t),
- kind_of_term (whd_betadeltaiota env ( 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. *)
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index b9503831c..7c6e54a9c 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -96,7 +96,7 @@ let interp_binder sigma env na t =
SPretyping.understand_tcc_evars 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 ( !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) ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 311889448..3d79508c3 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -75,7 +75,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
for i = 0 to lt-1 do
if not (e_cumul env evdref (vdefj.(i)).uj_type
(lift lt lar.(i))) then
- error_ill_typed_rec_body_loc loc env ( !evdref)
+ error_ill_typed_rec_body_loc loc env !evdref
i lna vdefj lar
done
@@ -207,12 +207,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 ( !evdref) ev) in
+ let hyps = evar_context (Evd.find !evdref 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 ( !evdref) c) in
+ let j = (Retyping.get_judgment_of env !evdref c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
| RPatVar (loc,(someta,n)) ->
@@ -281,8 +281,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 evdref names ftys vdefj;
- let ftys = Array.map (nf_evar ( !evdref)) ftys in
- let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in
+ let ftys = Array.map (nf_evar !evdref) ftys in
+ let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
let fixj = match fixkind with
| RFix (vn,i) ->
(* First, let's find the guard indexes. *)
@@ -332,7 +332,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) evdref resj in
- let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in
+ let resty = whd_betadeltaiota env !evdref resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
Option.iter (fun ty -> evdref :=
@@ -350,10 +350,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ ->
let hj = pretype empty_tycon env evdref lvar c in
error_cant_apply_not_functional_loc
- (join_loc floc argloc) env ( !evdref)
+ (join_loc floc argloc) env !evdref
resj [hj]
in
- let resj = j_nf_evar ( !evdref) (apply_rec env 1 fj ftycon args) in
+ let resj = j_nf_evar !evdref (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 ->
@@ -404,10 +404,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RLetTuple (loc,nal,(na,po),c,d) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env ( !evdref) cj.uj_type
+ try find_rectype env !evdref cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env ( !evdref) cj
+ error_case_not_inductive_loc cloc env !evdref cj
in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 1 then
@@ -431,14 +431,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 evdref lvar p in
- let ccl = nf_evar ( !evdref) pj.utj_val in
+ let ccl = nf_evar !evdref 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 ( !evdref) lp inst in
+ let fty = hnf_lam_applist env !evdref lp inst in
let fj = pretype (mk_tycon fty) env_f evdref lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let v =
@@ -451,12 +451,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f evdref lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
- let ccl = nf_evar ( !evdref) fj.uj_type in
+ let ccl = nf_evar !evdref 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 ( !evdref)
+ error_cant_find_case_type_loc loc env !evdref
cj.uj_val in
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
@@ -469,10 +469,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env ( !evdref) cj.uj_type
+ try find_rectype env !evdref cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env ( !evdref) cj in
+ error_case_not_inductive_loc cloc env !evdref cj in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 2 then
user_err_loc (loc,"",
@@ -491,7 +491,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 evdref lvar p in
- let ccl = nf_evar ( !evdref) pj.utj_val in
+ let ccl = nf_evar !evdref 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 evdref {uj_val = pred;
@@ -505,8 +505,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ())
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
- let pred = nf_evar ( !evdref) pred in
- let p = nf_evar ( !evdref) p in
+ let pred = nf_evar !evdref pred in
+ let p = nf_evar !evdref 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
@@ -560,7 +560,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RDynamic (loc,d) ->
if (Dyn.tag d) = "constr" then
let c = constr_out d in
- let j = (Retyping.get_judgment_of env ( !evdref) c) in
+ let j = (Retyping.get_judgment_of env !evdref c) in
j
(*inh_conv_coerce_to_tycon loc env evdref j tycon*)
else
@@ -596,7 +596,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
if e_cumul env evdref v tj.utj_val then tj
else
error_unexpected_type_loc
- (loc_of_rawconstr c) env ( !evdref) tj.utj_val v
+ (loc_of_rawconstr c) env !evdref tj.utj_val v
let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
let c' = match kind with
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6cb32a8ad..f10fcbc2c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -137,8 +137,8 @@ module Default = struct
(evd',{ uj_val = j.uj_val; uj_type = t })
| _ ->
let t,p =
- lookup_path_to_fun_from env ( evd) j.uj_type in
- (evd,apply_coercion env ( evd) p j t)
+ lookup_path_to_fun_from env evd j.uj_type in
+ (evd,apply_coercion env evd p j t)
let inh_app_fun env evd j =
try inh_app_fun env evd j
@@ -148,15 +148,15 @@ module Default = struct
let inh_tosort_force loc env evd j =
try
- let t,p = lookup_path_to_sort_from env ( evd) j.uj_type in
- let j1 = apply_coercion env ( evd) p j t in
- let j2 = on_judgment_type (whd_evar ( evd)) j1 in
+ let t,p = lookup_path_to_sort_from env evd j.uj_type in
+ let j1 = apply_coercion env evd p j t in
+ let j2 = on_judgment_type (whd_evar evd) j1 in
(evd,type_judgment env j2)
with Not_found ->
- error_not_a_type_loc loc env ( evd) j
+ error_not_a_type_loc loc env evd j
let inh_coerce_to_sort loc env evd j =
- let typ = whd_betadeltaiota env ( evd) j.uj_type in
+ let typ = whd_betadeltaiota env evd j.uj_type in
match kind_of_term typ with
| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
| Evar ev when not (is_defined_evar evd ev) ->
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index eca7c16f3..99cbfe498 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1497,7 +1497,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in
let cl' = {cl with evd = evd'} in
let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in
- let nf c = Evarutil.nf_evar ( cl'.evd) (Clenv.clenv_nf_meta cl' c) in
+ let nf c = Evarutil.nf_evar cl'.evd (Clenv.clenv_nf_meta cl' c) in
let c1 = if l2r then nf c' else nf c1
and c2 = if l2r then nf c2 else nf c'
and car = nf car and rel = nf rel in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 15:48:04 +0000