diff options
Diffstat (limited to 'pretyping/pretyping.mllib')
| -rw-r--r-- | pretyping/pretyping.mllib | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index a644e3d1..c8b3307d 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,7 +1,5 @@ Locusops -Termops -Namegen -Evd +Pretype_errors Reductionops Inductiveops Vnorm @@ -9,9 +7,8 @@ Arguments_renaming Nativenorm Retyping Cbv -Pretype_errors Find_subterm -Evarutil +Evardefine Evarsolve Recordops Evarconv |