aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml67
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/classes.ml4
-rw-r--r--toplevel/command.ml27
-rw-r--r--toplevel/record.ml6
-rw-r--r--toplevel/vernacentries.ml3
6 files changed, 64 insertions, 45 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 5f33ae834..5e686c41e 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -321,11 +321,12 @@ let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind
(* This function tryies to get the [inductive] between a constr
the constr should be Ind i or App(Ind i,[|args|])
*)
-let destruct_ind c =
- try let u,v = destApp c in
- let indc = destInd u in
+let destruct_ind sigma c =
+ let open EConstr in
+ try let u,v = destApp sigma c in
+ let indc = destInd sigma u in
indc,v
- with DestKO -> let indc = destInd c in
+ with DestKO -> let indc = destInd sigma c in
indc,[||]
(*
@@ -338,11 +339,12 @@ so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
*)
(* used in the leib -> bool side*)
let do_replace_lb mode lb_scheme_key aavoid narg p q =
+ let open EConstr in
let avoid = Array.of_list aavoid in
- let do_arg v offset =
+ let do_arg sigma v offset =
try
let x = narg*offset in
- let s = destVar v in
+ let s = destVar sigma v in
let n = Array.length avoid in
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
@@ -355,7 +357,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst v)) in
+ let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_lb")
@@ -364,7 +366,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
in
Proofview.Goal.nf_enter { enter = begin fun gl ->
let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
- let u,v = destruct_ind type_of_pq
+ let sigma = Tacmach.New.project gl in
+ let u,v = destruct_ind sigma type_of_pq
in let lb_type_of_p =
try
let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in
@@ -376,20 +379,20 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(str "Leibniz->boolean:" ++
str "You have to declare the" ++
str "decidability over " ++
- Printer.pr_constr type_of_pq ++
+ Printer.pr_econstr type_of_pq ++
str " first.")
in
Tacticals.New.tclZEROMSG err_msg
in
lb_type_of_p >>= fun (lb_type_of_p,eff) ->
+ Proofview.tclEVARMAP >>= fun sigma ->
let lb_args = Array.append (Array.append
(Array.map (fun x -> x) v)
- (Array.map (fun x -> do_arg x 1) v))
- (Array.map (fun x -> do_arg x 2) v)
- in let app = if Array.equal Term.eq_constr lb_args [||]
+ (Array.map (fun x -> do_arg sigma x 1) v))
+ (Array.map (fun x -> do_arg sigma x 2) v)
+ in let app = if Array.is_empty lb_args
then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
in
- let app = EConstr.of_constr app in
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
Equality.replace p q ; apply app ; Auto.default_auto]
@@ -397,13 +400,12 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(* used in the bool -> leib side *)
let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
- let lft = EConstr.Unsafe.to_constr lft in
- let rgt = EConstr.Unsafe.to_constr rgt in
+ let open EConstr in
let avoid = Array.of_list aavoid in
- let do_arg v offset =
+ let do_arg sigma v offset =
try
let x = narg*offset in
- let s = destVar v in
+ let s = destVar sigma v in
let n = Array.length avoid in
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
@@ -416,7 +418,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst v)) in
+ let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_bl")
@@ -427,13 +429,12 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) ->
- let t1 = EConstr.of_constr t1 in
- let t2 = EConstr.of_constr t2 in
Proofview.Goal.enter { enter = begin fun gl ->
let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
- if EConstr.eq_constr (Tacmach.New.project gl) t1 t2 then aux q1 q2
+ let sigma = Tacmach.New.project gl in
+ if EConstr.eq_constr sigma t1 t2 then aux q1 q2
else (
- let u,v = try destruct_ind tt1
+ let u,v = try destruct_ind sigma tt1
(* trick so that the good sequence is returned*)
with e when CErrors.noncritical e -> indu,[||]
in if eq_ind (fst u) ind
@@ -450,20 +451,19 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
(str "boolean->Leibniz:" ++
str "You have to declare the" ++
str "decidability over " ++
- Printer.pr_constr tt1 ++
+ Printer.pr_econstr tt1 ++
str " first.")
in
error err_msg
in let bl_args =
Array.append (Array.append
(Array.map (fun x -> x) v)
- (Array.map (fun x -> do_arg x 1) v))
- (Array.map (fun x -> do_arg x 2) v )
+ (Array.map (fun x -> do_arg sigma x 1) v))
+ (Array.map (fun x -> do_arg sigma x 2) v )
in
- let app = if Array.equal Term.eq_constr bl_args [||]
+ let app = if Array.is_empty bl_args
then bl_t1 else mkApp (bl_t1,bl_args)
in
- let app = EConstr.of_constr app in
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
Equality.replace_by t1 t2
@@ -475,21 +475,22 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
| ([],[]) -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
in
- begin try Proofview.tclUNIT (destApp lft)
+ Proofview.tclEVARMAP >>= fun sigma ->
+ begin try Proofview.tclUNIT (destApp sigma lft)
with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
end >>= fun (ind1,ca1) ->
- begin try Proofview.tclUNIT (destApp rgt)
+ begin try Proofview.tclUNIT (destApp sigma rgt)
with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
end >>= fun (ind2,ca2) ->
- begin try Proofview.tclUNIT (out_punivs (destInd ind1))
+ begin try Proofview.tclUNIT (out_punivs (destInd sigma ind1))
with DestKO ->
- begin try Proofview.tclUNIT (fst (fst (destConstruct ind1)))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind1)))
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp1,i1) ->
- begin try Proofview.tclUNIT (out_punivs (destInd ind2))
+ begin try Proofview.tclUNIT (out_punivs (destInd sigma ind2))
with DestKO ->
- begin try Proofview.tclUNIT (fst (fst (destConstruct ind2)))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind2)))
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp2,i2) ->
diff --git a/toplevel/class.ml b/toplevel/class.ml
index e55489471..4c7aa01cd 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -207,7 +207,7 @@ let build_id_coercion idf_opt source poly =
let _ =
if not
(Reductionops.is_conv_leq env sigma
- (EConstr.of_constr (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f))) (EConstr.of_constr typ_f))
+ (Typing.unsafe_type_of env sigma (EConstr.of_constr 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/classes.ml b/toplevel/classes.ml
index acfbce357..5087aa0c8 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -83,7 +83,7 @@ let type_ctx_instance evars env ctx inst subst =
let t' = substl subst (RelDecl.get_type decl) in
let c', l =
match decl with
- | LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
+ | LocalAssum _ -> EConstr.Unsafe.to_constr (interp_casted_constr_evars env evars (List.hd l) t'), List.tl l
| LocalDef (_,b,_) -> substl subst b, l
in
let d = RelDecl.get_name decl, Some c', t' in
@@ -151,6 +151,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let k, u, cty, ctx', ctx, len, imps, subst =
let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in
let c', imps' = interp_type_evars_impls ~impls env' evars tclass in
+ let c' = EConstr.Unsafe.to_constr c' in
let len = List.length ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum c' in
@@ -219,6 +220,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
| None -> if List.is_empty k.cl_props then Some (Inl subst) else None
| Some (Inr term) ->
let c = interp_casted_constr_evars env' evars term cty in
+ let c = EConstr.Unsafe.to_constr c in
Some (Inr (c, subst))
| Some (Inl props) ->
let get_id =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1fc89b8b0..7e3828131 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -103,6 +103,7 @@ let interp_definition pl bl p red_option c ctypopt =
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
+ let c = EConstr.Unsafe.to_constr c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
let vars = Universes.universes_of_constr body in
@@ -116,8 +117,10 @@ let interp_definition pl bl p red_option c ctypopt =
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
+ let c = EConstr.Unsafe.to_constr c in
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
+ let ty = EConstr.Unsafe.to_constr ty in
let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in
let beq b1 b2 = if b1 then b2 else not b2 in
let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
@@ -264,6 +267,7 @@ match local with
let interp_assumption evdref env impls bl c =
let c = prod_constr_expr c bl in
let ty, impls = interp_type_evars_impls env evdref ~impls c in
+ let ty = EConstr.Unsafe.to_constr ty in
let evd, nf = nf_evars_and_universes !evdref in
let ctx = Evd.universe_context_set evd in
((nf ty, ctx), impls)
@@ -318,6 +322,7 @@ let do_assumptions_bound_univs coe kind nl id pl c =
let evdref = ref (Evd.from_ctx ctx) in
let ty, impls = interp_type_evars_impls env evdref c in
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+ let ty = EConstr.Unsafe.to_constr ty in
let ty = nf ty in
let vars = Universes.universes_of_constr ty in
let evd = Evd.restrict_universe_context !evdref vars in
@@ -439,9 +444,10 @@ let interp_ind_arity env evdref ind =
let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
let pseudo_poly = check_anonymous_type c in
- let () = if not (Reduction.is_arity env t) then
+ let () = if not (Reductionops.is_arity env !evdref t) then
user_err ~loc:(constr_loc ind.ind_arity) (str "Not an arity")
in
+ let t = EConstr.Unsafe.to_constr t in
t, pseudo_poly, impls
let interp_cstrs evdref env impls mldata arity ind =
@@ -449,7 +455,7 @@ let interp_cstrs evdref env impls mldata arity ind =
(* Complete conclusions of constructor types if given in ML-style syntax *)
let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
(* Interpret the constructor types *)
- let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
+ let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls %> on_fst EConstr.Unsafe.to_constr) ctyps') in
(cnames, ctyps'', cimpls)
let sign_level env evd sign =
@@ -842,12 +848,14 @@ let interp_fix_context env evdref isfix fix =
((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
let interp_fix_ccl evdref impls (env,_) fix =
- interp_type_evars_impls ~impls env evdref fix.fix_type
+ let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in
+ (EConstr.Unsafe.to_constr c, impl)
let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
Option.map (fun body ->
let env = push_rel_context ctx env_rec in
let body = interp_casted_constr_evars env evdref ~impls body ccl in
+ let body = EConstr.Unsafe.to_constr body in
it_mkLambda_or_LetIn body ctx) fix.fix_body
let build_fix_type (_,ctx) ccl = Term.it_mkProd_or_LetIn ccl ctx
@@ -946,6 +954,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let len = List.length binders_rel in
let top_env = push_rel_context binders_rel env in
let top_arity = interp_type_evars top_env evdref arityc in
+ let top_arity = EConstr.Unsafe.to_constr top_arity in
let full_arity = Term.it_mkProd_or_LetIn top_arity binders_rel in
let argtyp, letbinders, make = telescope binders_rel in
let argname = Id.of_string "recarg" in
@@ -953,22 +962,24 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let binders = letbinders @ [arg] in
let binders_env = push_rel_context binders_rel env in
let rel, _ = interp_constr_evars_impls env evdref r in
- let relty = Typing.unsafe_type_of env !evdref (EConstr.of_constr rel) in
+ let relty = Typing.unsafe_type_of env !evdref rel in
let relargty =
let error () =
user_err ~loc:(constr_loc r)
~hdr:"Command.build_wellfounded"
- (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
+ (Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
in
try
- let ctx, ar = Reductionops.splay_prod_n env !evdref 2 (EConstr.of_constr relty) in
+ let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
match ctx, EConstr.kind !evdref ar with
| [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
when Reductionops.is_conv env !evdref (EConstr.of_constr t) (EConstr.of_constr u) -> t
| _, _ -> error ()
with e when CErrors.noncritical e -> error ()
in
+ let rel = EConstr.Unsafe.to_constr rel in
let measure = interp_casted_constr_evars binders_env evdref measure relargty in
+ let measure = EConstr.Unsafe.to_constr measure in
let wf_rel, wf_rel_fun, measure_fn =
let measure_body, measure =
it_mkLambda_or_LetIn measure letbinders,
@@ -1025,6 +1036,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
interp_casted_constr_evars (push_rel_context ctx env) evdref
~impls:newimpls body (lift 1 top_arity)
in
+ let intern_body = EConstr.Unsafe.to_constr intern_body in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let def =
@@ -1035,6 +1047,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
prop |])
in
let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in
+ let def = EConstr.Unsafe.to_constr def in
let _ = evdref := Evarutil.nf_evar_map !evdref in
let def = mkApp (def, [|intern_body_lam|]) in
let binders_rel = nf_evar_context !evdref binders_rel in
@@ -1110,7 +1123,7 @@ let interp_recursive isfix fixl notations =
let fixprot =
try
let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
- Typing.e_solve_evars env evdref (EConstr.of_constr app)
+ EConstr.Unsafe.to_constr (Typing.e_solve_evars env evdref (EConstr.of_constr app))
with e when CErrors.noncritical e -> t
in
LocalAssum (id,fixprot) :: env'
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 73035deb0..a65f5252e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -66,7 +66,8 @@ let interp_fields_evars env evars impls_env nots l =
List.fold_left2
(fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
let t', impl = interp_type_evars_impls env evars ~impls t in
- let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
+ let b' = Option.map (fun x -> EConstr.Unsafe.to_constr (fst (interp_casted_constr_evars_impls env evars ~impls x t'))) b in
+ let t' = EConstr.Unsafe.to_constr t' in
let impls =
match i with
| Anonymous -> impls
@@ -120,7 +121,8 @@ 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 (EConstr.of_constr s) in
+ let sred = Reductionops.whd_all env !evars s in
+ let s = EConstr.Unsafe.to_constr s in
let sred = EConstr.Unsafe.to_constr sred in
(match kind_of_term sred with
| Sort s' ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ee2aacfc5..4376f51dc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -108,7 +108,7 @@ let show_intro all =
let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
if not (List.is_empty gls) then begin
let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
- let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (EConstr.of_constr (pf_concl gl))) in
+ let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
if all then
let lid = Tactics.find_intro_names l gl in
Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid))
@@ -1572,6 +1572,7 @@ let get_current_context_of_args = function
let vernac_check_may_eval redexp glopt rc =
let (sigma, env) = get_current_context_of_args glopt in
let sigma', c = interp_open_constr env sigma rc in
+ let c = EConstr.Unsafe.to_constr c in
let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
Evarconv.check_problems_are_solved env sigma';
let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 12:18:52 +0000