diff options
| author | Pierre-Marie Pédrot | 2018-11-20 14:10:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-20 14:10:16 +0100 |
| commit | 4735f7d9da506a64c63680c4630e1f32945d24dc (patch) | |
| tree | 881a246330100ee961801e89113d3df48d95b8f3 /tactics | |
| parent | 1595aa8045e7076aa51b58f80173dd245303bed6 (diff) | |
| parent | 758041989f29ed960eba8bf7fe0d232d3937db60 (diff) | |
Merge PR #8982: [proof] Provide better control of "open proofs" exceptions.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1bb33f2a23..5959dd54b1 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -358,7 +358,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Eauto.registered_e_assumption :: (tclTHEN Tactics.intro trivial_fail :: [trivial_resolve]) in - tclFIRST (List.map tclCOMPLETE tacl) + tclSOLVE tacl and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl = let open Proofview.Notations in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9a6bdab7b9..63ef4f850f 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -151,7 +151,7 @@ let rec e_trivial_fail_db db_list local_db = (Tacticals.New.tclTHEN Tactics.intro next) :: (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) in - Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) + Tacticals.New.tclSOLVE tacl end and e_my_find_search env sigma db_list local_db secvars hdc concl = |