aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mllib
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/pretyping.mllib
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/pretyping.mllib')
-rw-r--r--pretyping/pretyping.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index b0d5a1df6..e8c0bbbf9 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -9,6 +9,7 @@ Cbv
Pretype_errors
Find_subterm
Evarutil
+Evardefine
Evarsolve
Recordops
Evarconv