diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 20:41:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 21:03:32 +0100 |
| commit | c3de822e711fa3f10817432b7023fc2f88c0aeeb (patch) | |
| tree | 5c9f9713cb09aa63c2351a994cd9b8b62d8a8715 /pretyping/pretyping.mllib | |
| parent | e98d7276f52c4b67bf05a80a6b44f334966f82fd (diff) | |
Making Evarutil independent from Reductionops.
Diffstat (limited to 'pretyping/pretyping.mllib')
| -rw-r--r-- | pretyping/pretyping.mllib | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index e8c0bbbf9..be517d1aa 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,4 +1,6 @@ Locusops +Pretype_errors +Evarutil Reductionops Inductiveops Vnorm @@ -6,9 +8,7 @@ Arguments_renaming Nativenorm Retyping Cbv -Pretype_errors Find_subterm -Evarutil Evardefine Evarsolve Recordops |