diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-22 00:07:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 368a25e4ef14512b00f5799e26c3f615bc540201 (patch) | |
| tree | 29602372307ff70f2a7b06f0a27609a73caa5666 /tactics/eqdecide.ml | |
| parent | 36a98d55576ebdb106a55c3bd682961da8d77dee (diff) | |
[api] Misctypes removal: several moves:
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 176701d99..832014a61 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -24,11 +24,11 @@ open Tactics open Tacticals.New open Auto open Constr_matching -open Misctypes open Hipattern open Proofview.Notations open Tacmach.New open Coqlib +open Tactypes (* This file containts the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the @@ -58,14 +58,14 @@ let clear_last = let choose_eq eqonleft = if eqonleft then - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings else - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings let choose_noteq eqonleft = if eqonleft then - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings else - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) |