diff options
| author | Pierre-Marie Pédrot | 2018-11-07 11:42:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-07 11:42:38 +0100 |
| commit | 19b7ce2f39eaf37e48d1d12ef73defab3c9fbdb2 (patch) | |
| tree | a55af313e25a17382c94a60805b95e82f02ef6c6 /vernac | |
| parent | e857efb2e61c29a5b0b29702ca8d746ea2580ca6 (diff) | |
| parent | 7f2946157797ba7da3ed8712c10f5a0302b36d49 (diff) | |
Merge PR #8773: [checker] Refactor by sharing code with the kernel
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 6 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ad6ca3a84e..ba31f73030 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -201,8 +201,8 @@ let explain_elim_arity env sigma ind sorts c pj okinds = let pc = pr_leconstr_env env sigma c in let msg = match okinds with | Some(kp,ki,explanation) -> - let pki = pr_sort_family ki in - let pkp = pr_sort_family kp in + let pki = Sorts.pr_sort_family ki in + let pkp = Sorts.pr_sort_family kp in let explanation = match explanation with | NonInformativeToInformative -> "proofs can be eliminated only to build proofs" @@ -210,7 +210,7 @@ let explain_elim_arity env sigma ind sorts c pj okinds = "strong elimination on non-small inductive types leads to paradoxes" | WrongArity -> "wrong arity" in - let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in + let ppar = pr_disjunction (fun s -> quote (Sorts.pr_sort_family s)) sorts in let ppt = pr_leconstr_env env sigma (snd (decompose_prod_assum sigma pj.uj_type)) in hov 0 (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++ diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index a0e8f38c0b..1c1faca599 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -312,7 +312,7 @@ open Pputils ) ++ hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) + hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s) | CaseScheme (dep,ind,s) -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() @@ -320,7 +320,7 @@ open Pputils ) ++ hov 0 ((if dep then keyword "Elimination for" else keyword "Case for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) + hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s) | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() |