aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 36273faae..714cd8634 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -773,7 +773,7 @@ let rec take_tac wits gls =
match wits with
[] -> tclIDTAC gls
| wit::rest ->
- let typ = pf_type_of gls wit in
+ let typ = pf_unsafe_type_of gls wit in
tclTHEN (thus_tac wit typ []) (take_tac rest) gls
@@ -854,7 +854,7 @@ let start_tree env ind rp =
let build_per_info etype casee gls =
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls casee in
let is_dep = dependent casee concl in
let hd,args = decompose_app (special_whd gls ctyp) in
let (ind,u) =
@@ -869,7 +869,7 @@ let build_per_info etype casee gls =
| _ -> mind.mind_nparams,None in
let params,real_args = List.chop nparams args in
let abstract_obj c body =
- let typ=pf_type_of gls c in
+ let typ=pf_unsafe_type_of gls c in
lambda_create env (typ,subst_term c body) in
let pred= List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term casee concl)) in
@@ -1228,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
let nparams = mind.mind_nparams in
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls casee in
let hd,all_args = decompose_app (special_whd gls ctyp) in
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
+ let typ=pf_unsafe_type_of gls c in
lambda_create env (typ,subst_term c body) in
let elim_pred = List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term casee concl)) in