aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-25 14:31:15 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:42:01 +0200
commit87910d7be9bd50de4db80f70c6e287c7c7994460 (patch)
treeff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /engine
parent5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff)
Fix 4.04 warnings
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 6b1e1a855..db048bbd6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -15,7 +15,7 @@ open Term
open Vars
open Environ
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
module NamedDecl = Context.Named.Declaration
(** Generic filters *)