diff options
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index b62bf5820..7a6b07d38 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -94,7 +94,7 @@ let e_split = e_constructor_tac (Some 1) 1 TACTIC EXTEND econstructor [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ] | [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ] -| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_map Tacinterp.eval_tactic t) ] +| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (Option.map Tacinterp.eval_tactic t) ] END TACTIC EXTEND eleft @@ -192,7 +192,7 @@ and e_my_find_search db_list local_db hdc concl = (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl - (out_some p) tacast + (Option.get p) tacast in (tac,fmt_autotactic t)) (*i |