diff options
author | 2015-12-03 20:10:26 +0100 | |
---|---|---|
committer | 2015-12-03 20:10:26 +0100 | |
commit | f135a3967ca3d22bdc5566a54f042ba5bd6a343c (patch) | |
tree | 26347ce986527296f38d664743644a6fd00ce360 /tactics | |
parent | 06a30c78c6148e8286c0904368bcc0f7c5af2c81 (diff) |
Fixing Tauto compilation for older versions of OCaml.
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tauto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index a96adcca8..a3894a913 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -14,6 +14,7 @@ open Names open Pp open Genarg open Stdarg +open Tacexpr open Tacinterp open Tactics open Errors @@ -93,7 +94,6 @@ let make_lfun l = List.fold_left fold Id.Map.empty l let tacticIn tac name = - let open Tacexpr in let name = { mltac_plugin = "tauto"; mltac_tactic = name; } in let entry = { mltac_name = name; mltac_index = 0 } in let tac _ ist = |