diff options
| author | Gaetan Gilbert | 2017-04-25 14:31:15 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-04-27 21:42:01 +0200 |
| commit | 87910d7be9bd50de4db80f70c6e287c7c7994460 (patch) | |
| tree | ff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /plugins/ltac | |
| parent | 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff) | |
Fix 4.04 warnings
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tauto.ml | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 12a1566e20..9a1615d3f2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -39,7 +39,7 @@ open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) (** Typeclass-based generalized rewriting. *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index e86d1c7283..4de2081cf8 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -10,7 +10,6 @@ open Term open EConstr open Hipattern open Names -open Pp open Geninterp open Misctypes open Tacexpr |