diff options
| author | Maxime Dénès | 2018-10-09 18:21:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-06 14:19:37 +0100 |
| commit | a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3 (patch) | |
| tree | cc247d4ae7a66223add8ea189ca63125edd7d64e /plugins | |
| parent | 58f891c100d1a1821ed6385c1d06f9e0a77ecdac (diff) | |
[checker] Refactor by sharing code with the kernel
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 857215751a..155df1c1e0 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -197,7 +197,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ - Termops.pr_sort_family s + Sorts.pr_sort_family s } |