diff options
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 10 |
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 |