aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-20 20:11:50 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-20 20:38:41 +0100
commite98d7276f52c4b67bf05a80a6b44f334966f82fd (patch)
treee85396003f974d5eaa8f84722c0ca3f050990da1 /pretyping/cases.ml
parent08c31f46aa05098e1a97d9144599c1e5072b7fc3 (diff)
Splitting Evarutil in two distinct files.
Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8a55a7aaa..c3968f896 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -25,6 +25,7 @@ open Glob_ops
open Retyping
open Pretype_errors
open Evarutil
+open Evardefine
open Evarsolve
open Evarconv
open Evd