diff options
Diffstat (limited to 'plugins/ltac/tauto.ml')
| -rw-r--r-- | plugins/ltac/tauto.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 8eeb8903e..368c20469 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -94,7 +94,7 @@ let clear id = Tactics.clear [id] let assumption = Tactics.assumption -let split = Tactics.split_with_bindings false [Misctypes.NoBindings] +let split = Tactics.split_with_bindings false [Tactypes.NoBindings] (** Test *) @@ -175,7 +175,7 @@ let flatten_contravariant_disj _ ist = | Some (_,args) -> let map i arg = let typ = mkArrow arg c in - let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in + let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in let by = tclTHENLIST [intro; apply hyp; ci; assumption] in assert_ ~by typ in |