aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_interp.ml26
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml31
-rw-r--r--plugins/decl_mode/g_decl_mode.ml44
3 files changed, 31 insertions, 30 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 505d7dba5c..e0aee15e60 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -144,26 +144,26 @@ let intern_proof_instr globs instr=
(* INTERP *)
let interp_justification_items sigma env =
- Option.map (List.map (fun c ->understand sigma env (fst c)))
+ Option.map (List.map (fun c -> fst (*FIXME*)(understand sigma env (fst c))))
let interp_constr check_sort sigma env c =
if check_sort then
- understand sigma env ~expected_type:IsType (fst c)
+ fst (understand sigma env ~expected_type:IsType (fst c) (* FIXME *))
else
- understand sigma env (fst c)
+ fst (understand sigma env (fst c))
let special_whd env =
let infos=Closure.create_clos_infos Closure.betadeltaiota env in
(fun t -> Closure.whd_val infos (Closure.inject t))
-let _eq = Globnames.constr_of_global (Coqlib.glob_eq)
+let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
let decompose_eq env id =
let typ = Environ.named_type id env in
let whd = special_whd env typ in
match kind_of_term whd with
App (f,args)->
- if eq_constr f _eq && Int.equal (Array.length args) 3
+ if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
then args.(0)
else error "Previous step is not an equality."
| _ -> error "Previous step is not an equality."
@@ -173,7 +173,7 @@ let get_eq_typ info env =
typ
let interp_constr_in_type typ sigma env c =
- understand sigma env (fst c) ~expected_type:(OfType typ)
+ fst (understand sigma env (fst c) ~expected_type:(OfType typ))(*FIXME*)
let interp_statement interp_it sigma env st =
{st_label=st.st_label;
@@ -213,7 +213,7 @@ let rec match_hyps blend names constr = function
qhyp::rhyps,head
let interp_hyps_gen inject blend sigma env hyps head =
- let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in
+ let constr= fst(*FIXME*) (understand sigma env (glob_constr_of_hyps inject hyps head)) in
match_hyps blend [] constr hyps
let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop)
@@ -246,7 +246,7 @@ let rec glob_of_pat =
add_params (pred n) (GHole(Loc.ghost,
Evar_kinds.TomatchTypeParameter(ind,n), None)::q) in
let args = List.map glob_of_pat lpat in
- glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr),
+ glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None),
add_params mind.Declarations.mind_nparams args)
let prod_one_hyp = function
@@ -333,7 +333,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
(if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
str "expected.") in
let app_ind =
- let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in
+ let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in
let rparams = List.map detype_ground pinfo.per_params in
let rparams_rec =
List.map
@@ -365,7 +365,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
let term3=List.fold_right let_in_one_alias aliases term2 in
let term4=List.fold_right prod_one_id loc_ids term3 in
let term5=List.fold_right prod_one_hyp params term4 in
- let constr = understand sigma env term5 in
+ let constr = fst (understand sigma env term5)(*FIXME*) in
let tparams,nam4,rest4 = match_args destProd [] constr params in
let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
@@ -409,7 +409,7 @@ let interp_suffices_clause sigma env (hyps,cot)=
nenv,res
let interp_casee sigma env = function
- Real c -> Real (understand sigma env (fst c))
+ Real c -> Real (fst (understand sigma env (fst c)))(*FIXME*)
| Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut)
let abstract_one_arg = function
@@ -425,7 +425,7 @@ let glob_constr_of_fun args body =
List.fold_right abstract_one_arg args (fst body)
let interp_fun sigma env args body =
- let constr=understand sigma env (glob_constr_of_fun args body) in
+ let constr=fst (*FIXME*) (understand sigma env (glob_constr_of_fun args body)) in
match_args destLambda [] constr args
let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function
@@ -448,7 +448,7 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu
let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in
Pcase (tparams,tpat,thyps)
| Ptake witl ->
- Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
+ Ptake (List.map (fun c -> fst (*FIXME*) (understand sigma env (fst c))) witl)
| Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c,
interp_hyps sigma env hyps)
| Pper (et,c) -> Pper (et,interp_casee sigma env c)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index de57330ecf..8647ca6769 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -292,13 +292,13 @@ let rec replace_in_list m l = function
let enstack_subsubgoals env se stack gls=
let hd,params = decompose_app (special_whd gls se.se_type) in
match kind_of_term hd with
- Ind ind when is_good_inductive env ind ->
+ Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *)
let mib,oib=
Inductive.lookup_mind_specif env ind in
let gentypes=
- Inductive.arities_of_constructors ind (mib,oib) in
+ Inductive.arities_of_constructors indu (mib,oib) in
let process i gentyp =
- let constructor = mkConstruct(ind,succ i)
+ let constructor = mkConstructU ((ind,succ i),u)
(* constructors numbering*) in
let appterm = applist (constructor,params) in
let apptype = prod_applist gentyp params in
@@ -357,7 +357,7 @@ let find_subsubgoal c ctyp skip submetas gls =
try
let unifier =
Unification.w_unify env se.se_evd Reduction.CUMUL
- ~flags:Unification.elim_flags ctyp se.se_type in
+ ~flags:(Unification.elim_flags ()) ctyp se.se_type in
if n <= 0 then
{se with
se_evd=meta_assign se.se_meta
@@ -488,14 +488,14 @@ let instr_cut mkstat _thus _then cut gls0 =
(* iterated equality *)
-let _eq = Globnames.constr_of_global (Coqlib.glob_eq)
+let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
let decompose_eq id gls =
let typ = pf_get_hyp_typ gls id in
let whd = (special_whd gls typ) in
match kind_of_term whd with
App (f,args)->
- if eq_constr f _eq && Int.equal (Array.length args) 3
+ if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
then (args.(0),
args.(1),
args.(2))
@@ -530,14 +530,14 @@ let instr_rew _thus rew_side cut gls0 =
else tclIDTAC gls in
match rew_side with
Lhs ->
- let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
+ let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in
tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
[tclTHEN tcl_erase_info
(tclTHENS (Proofview.V82.of_tactic (transitivity lhs))
[just_tac;exact_check (mkVar last_id)]);
thus_tac new_eq] gls0
| Rhs ->
- let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
+ let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
[tclTHEN tcl_erase_info
(tclTHENS (Proofview.V82.of_tactic (transitivity rhs))
@@ -663,11 +663,11 @@ let conjunction_arity id gls =
let hd,params = decompose_app (special_whd gls typ) in
let env =pf_env gls in
match kind_of_term hd with
- Ind ind when is_good_inductive env ind ->
+ Ind (ind,u as indu) when is_good_inductive env ind ->
let mib,oib=
Inductive.lookup_mind_specif env ind in
let gentypes=
- Inductive.arities_of_constructors ind (mib,oib) in
+ Inductive.arities_of_constructors indu (mib,oib) in
let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in
let apptype = prod_applist gentypes.(0) params in
let rc,_ = Reduction.dest_prod env apptype in
@@ -832,7 +832,7 @@ let build_per_info etype casee gls =
let ctyp=pf_type_of gls casee in
let is_dep = dependent casee concl in
let hd,args = decompose_app (special_whd gls ctyp) in
- let ind =
+ let (ind,u as indu) =
try
destInd hd
with DestKO ->
@@ -1031,7 +1031,7 @@ let rec st_assoc id = function
let thesis_for obj typ per_info env=
let rc,hd1=decompose_prod typ in
let cind,all_args=decompose_app typ in
- let ind = destInd cind in
+ let ind,u = destInd cind in
let _ = if not (eq_ind ind per_info.per_ind) then
errorlabstrm "thesis_for"
((Printer.pr_constr_env env obj) ++ spc () ++
@@ -1166,7 +1166,7 @@ let hrec_for fix_id per_info gls obj_id =
let typ=pf_get_hyp_typ gls obj_id in
let rc,hd1=decompose_prod typ in
let cind,all_args=decompose_app typ in
- let ind = destInd cind in assert (eq_ind ind per_info.per_ind);
+ let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind);
let params,args= List.chop per_info.per_nparams all_args in
assert begin
try List.for_all2 eq_constr params per_info.per_params with
@@ -1205,7 +1205,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
let env=pf_env gls in
let ctyp=pf_type_of gls casee in
let hd,all_args = decompose_app (special_whd gls ctyp) in
- let _ = assert (eq_ind (destInd hd) ind) in (* just in case *)
+ let ind', u = destInd hd in
+ let _ = assert (eq_ind ind' ind) in (* just in case *)
let params,real_args = List.chop nparams all_args in
let abstract_obj c body =
let typ=pf_type_of gls c in
@@ -1213,7 +1214,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
let elim_pred = List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term casee concl)) in
let case_info = Inductiveops.make_case_info env ind RegularStyle in
- let gen_arities = Inductive.arities_of_constructors ind spec in
+ let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
let f_ids typ =
let sign =
(prod_assum (prod_applist typ params)) in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 7c9ef3c2a8..36abb86cc0 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -176,7 +176,7 @@ GLOBAL: proof_instr;
statement :
[[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
| i=ident -> {st_label=Anonymous;
- st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i))}
+ st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)}
| c=constr -> {st_label=Anonymous;st_it=c}
]];
constr_or_thesis :
@@ -189,7 +189,7 @@ GLOBAL: proof_instr;
|
[ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
| i=ident -> {st_label=Anonymous;
- st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i)))}
+ st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))}
| c=constr -> {st_label=Anonymous;st_it=This c}
]
];
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:27:03 +0000