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 /tactics/class_tactics.ml | |
| 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 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3fafbe15a1..e1fe51656f 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -149,7 +149,7 @@ let e_give_exact flags poly (c,clenv) gl = c, {gl with sigma = clenv'.evd} else c, gl in - let t1 = pf_type_of gl c in + let t1 = pf_unsafe_type_of gl c in tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = @@ -168,7 +168,7 @@ let unify_resolve poly flags (c,clenv) gls = let clenv_of_prods poly nprods (c, clenv) gls = if poly || Int.equal nprods 0 then Some clenv else - let ty = pf_type_of gls c in + let ty = pf_unsafe_type_of gls c in let diff = nb_prod ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) @@ -231,13 +231,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl = | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) | Extern tacast -> conclPattern concl p tacast in - let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in + let tac = Proofview.V82.of_tactic (run_hint t tac) in let tac = if complete then tclCOMPLETE tac else tac in - match repr_auto_tactic t with - | Extern _ -> (tac,b,true, name, lazy (pr_autotactic t)) + match repr_hint t with + | Extern _ -> (tac,b,true, name, lazy (pr_hint t)) | _ -> (* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) - (tac,b,false, name, lazy (pr_autotactic t)) + (tac,b,false, name, lazy (pr_hint t)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db sigma concl = @@ -842,6 +842,6 @@ let is_ground c gl = let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_type_of gl c in + let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in unify_e_resolve false flags (c,ce) gl |