diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-14 20:44:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:38 +0200 |
| commit | d5fece25d8964d5d9fcd55b66164286aeef5fb9f (patch) | |
| tree | 60d584831ef3574c8d07daaef85929bd81a12d88 /plugins/btauto | |
| parent | 4684ae383a6ee56b4717026479eceb3b41b45ab0 (diff) | |
Reorganization of tactics:
- made "apply" tactics of type Proofview.tactic, as well as other inner
functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
pattern (doc not changed)
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index dbd89019e..e6a841153 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -248,7 +248,7 @@ module Btauto = struct let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (Tactics.change_concl changed_gl); - Proofview.V82.tactic (Tactics.apply (Lazy.force soundness)); + Tactics.apply (Lazy.force soundness); Proofview.V82.tactic (Tactics.normalise_vm_in_concl); try_unification env ] |