aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml10
-rw-r--r--toplevel/class.ml4
-rw-r--r--toplevel/command.ml8
-rw-r--r--toplevel/himsg.ml6
-rw-r--r--toplevel/obligations.ml6
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacentries.ml2
7 files changed, 19 insertions, 19 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b1811d6a6..02c43aec5 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -180,7 +180,7 @@ let build_beq_scheme mode kn =
let lifti = ndx in
let rec aux c =
let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
- match kind_of_term c with
+ match EConstr.kind Evd.empty (** FIXME *) c with
| Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
| Var x ->
let eid = id_of_string ("eq_"^(string_of_id x)) in
@@ -189,7 +189,7 @@ let build_beq_scheme mode kn =
with Not_found -> raise (ParameterWithoutEquality (VarRef x))
in
mkVar eid, Safe_typing.empty_private_constants
- | Cast (x,_,_) -> aux (applist (x,a))
+ | Cast (x,_,_) -> aux (EConstr.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
@@ -205,7 +205,7 @@ let build_beq_scheme mode kn =
in
let args =
Array.append
- (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
+ (Array.of_list (List.map (fun x -> lift lifti (EConstr.Unsafe.to_constr x)) a)) eqa in
if Int.equal (Array.length args) 0 then eq, eff
else mkApp (eq, args), eff
with Not_found -> raise(EqNotFound (ind', fst ind))
@@ -217,7 +217,7 @@ let build_beq_scheme mode kn =
| Const kn ->
(match Environ.constant_opt_value_in env kn with
| None -> raise (ParameterWithoutEquality (ConstRef (fst kn)))
- | Some c -> aux (applist (c,a)))
+ | Some c -> aux (EConstr.applist (EConstr.of_constr c,a)))
| Proj _ -> raise (EqUnknown "Proj")
| Construct _ -> raise (EqUnknown "Construct")
| Case _ -> raise (EqUnknown "Case")
@@ -261,7 +261,7 @@ let build_beq_scheme mode kn =
nparrec
(nparrec+3+2*nb_cstr_args)
(nb_cstr_args+ndx+1)
- cc
+ (EConstr.of_constr cc)
in
eff := Safe_typing.concat_private eff' !eff;
Array.set eqs ndx
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 46854e5c0..5aa000b16 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -62,7 +62,7 @@ let explain_coercion_error g = function
(* Verifications pour l'ajout d'une classe *)
let check_reference_arity ref =
- if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global_unsafe ref)) then
+ if not (Reductionops.is_arity (Global.env()) Evd.empty (EConstr.of_constr (Global.type_of_global_unsafe ref))) (** FIXME *) then
raise (CoercionError (NotAClass ref))
let check_arity = function
@@ -206,7 +206,7 @@ let build_id_coercion idf_opt source poly =
let _ =
if not
(Reductionops.is_conv_leq env sigma
- (Typing.unsafe_type_of env sigma val_f) typ_f)
+ (EConstr.of_constr (Typing.unsafe_type_of env sigma val_f)) (EConstr.of_constr typ_f))
then
user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 62bbd4b97..249d41845 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -45,7 +45,7 @@ let do_universe poly l = Declare.do_universe poly l
let do_constraint poly l = Declare.do_constraint poly l
let rec under_binders env sigma f n c =
- if Int.equal n 0 then f env sigma c else
+ if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
match kind_of_term c with
| Lambda (x,t,c) ->
mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
@@ -395,7 +395,7 @@ let check_all_names_different indl =
| _ -> raise (InductiveError (SameNamesOverlap l))
let mk_mltype_data evdref env assums arity indname =
- let is_ml_type = is_sort env !evdref arity in
+ let is_ml_type = is_sort env !evdref (EConstr.of_constr arity) in
(is_ml_type,indname,assums)
let prepare_param = function
@@ -961,10 +961,10 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
(Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
in
try
- let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
+ let ctx, ar = Reductionops.splay_prod_n env !evdref 2 (EConstr.of_constr relty) in
match ctx, kind_of_term ar with
| [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
- when Reductionops.is_conv env !evdref t u -> t
+ when Reductionops.is_conv env !evdref (EConstr.of_constr t) (EConstr.of_constr u) -> t
| _, _ -> error ()
with e when CErrors.noncritical e -> error ()
in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index bfe86053e..0279ff0c5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -79,7 +79,7 @@ let rec contract3' env a b c = function
let j_nf_betaiotaevar sigma j =
{ uj_val = Evarutil.nf_evar sigma j.uj_val;
- uj_type = Reductionops.nf_betaiota sigma j.uj_type }
+ uj_type = Reductionops.nf_betaiota sigma (EConstr.of_constr j.uj_type) }
let jv_nf_betaiotaevar sigma jl =
Array.map (j_nf_betaiotaevar sigma) jl
@@ -335,7 +335,7 @@ let explain_unification_error env sigma p1 p2 = function
let explain_actual_type env sigma j t reason =
let env = make_all_name_different env in
let j = j_nf_betaiotaevar sigma j in
- let t = Reductionops.nf_betaiota sigma t in
+ let t = Reductionops.nf_betaiota sigma (EConstr.of_constr t) in
(** Actually print *)
let pe = pr_ne_context_of (str "In environment") env sigma in
let pc = pr_lconstr_env env sigma (Environ.j_val j) in
@@ -351,7 +351,7 @@ let explain_actual_type env sigma j t reason =
let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let randl = jv_nf_betaiotaevar sigma randl in
let exptyp = Evarutil.nf_evar sigma exptyp in
- let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
+ let actualtyp = Reductionops.nf_betaiota sigma (EConstr.of_constr actualtyp) in
let rator = Evarutil.j_nf_evar sigma rator in
let env = make_all_name_different env in
let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 1d5e4a2fa..8aee9d241 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -264,7 +264,7 @@ let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)
let reduce c =
- Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c
+ Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c)
exception NoObligations of Id.t option
@@ -534,8 +534,8 @@ let declare_mutual_definition l =
List.split3
(List.map (fun x ->
let subs, typ = (subst_body true x) in
- let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
- let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
+ let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len (EConstr.of_constr subs)) in
+ let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len (EConstr.of_constr typ)) in
x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 7dee4aae0..ffe7980ef 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -120,7 +120,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
match t with
| CSort (_, Misctypes.GType []) -> true | _ -> false in
let s = interp_type_evars env evars ~impls:empty_internalization_env t in
- let sred = Reductionops.whd_all env !evars s in
+ let sred = Reductionops.whd_all env !evars (EConstr.of_constr s) in
(match kind_of_term sred with
| Sort s' ->
(if poly then
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bbbdbdb67..593aa9578 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1586,7 +1586,7 @@ let vernac_check_may_eval redexp glopt rc =
match redexp with
| None ->
let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
- let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
+ let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' (EConstr.of_constr j.Environ.uj_type) } in
Feedback.msg_notice (print_judgment env sigma' j ++
pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
Printer.pr_universe_ctx sigma uctx)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:44:13 +0000