diff options
| author | Hugo Herbelin | 2015-05-15 11:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-15 11:39:49 +0200 |
| commit | 5d015ae0d90fd7fd3d440acee6ccd501d8b63ba0 (patch) | |
| tree | e73fb685fea3bd4aa5a9eecde1df69c518acccf0 /plugins/decl_mode | |
| parent | 76c3b40482978fffca50f6f59e8bcae455680aba (diff) | |
| parent | 3fb81febe8efc34860688cac88a2267cfe298cf7 (diff) | |
Merge v8.5 into trunk
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
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 36273faae2..714cd86341 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 |