aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/rewrite.ml
diff options
context:
space:
mode:
authorGaetan Gilbert2017-04-25 14:31:15 +0200
committerGaetan Gilbert2017-04-27 21:42:01 +0200
commit87910d7be9bd50de4db80f70c6e287c7c7994460 (patch)
treeff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /plugins/ltac/rewrite.ml
parent5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff)
Fix 4.04 warnings
Diffstat (limited to 'plugins/ltac/rewrite.ml')
-rw-r--r--plugins/ltac/rewrite.ml2
1 files changed, 1 insertions, 1 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. *)