aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-03-20 20:11:50 +0100
committerPierre-Marie Pédrot2016-03-20 20:38:41 +0100
commite98d7276f52c4b67bf05a80a6b44f334966f82fd (patch)
treee85396003f974d5eaa8f84722c0ca3f050990da1 /dev
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 'dev')
-rw-r--r--dev/printers.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index db86bb5edd..4830b36ab5 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -131,6 +131,7 @@ Retyping
Cbv
Pretype_errors
Evarutil
+Evardefine
Evarsolve
Recordops
Evarconv