diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-03 20:10:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-03 20:10:26 +0100 |
| commit | f135a3967ca3d22bdc5566a54f042ba5bd6a343c (patch) | |
| tree | 26347ce986527296f38d664743644a6fd00ce360 /tactics/tauto.ml4 | |
| parent | 06a30c78c6148e8286c0904368bcc0f7c5af2c81 (diff) | |
Fixing Tauto compilation for older versions of OCaml.
Diffstat (limited to 'tactics/tauto.ml4')
| -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 = |