aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.ml
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 /pretyping/evarsolve.ml
parent5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff)
Fix 4.04 warnings
Diffstat (limited to 'pretyping/evarsolve.ml')
-rw-r--r--pretyping/evarsolve.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 77086d046..f0d011477 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module CVars = Vars
open Util
open CErrors
open Names