From 58f891c100d1a1821ed6385c1d06f9e0a77ecdac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 6 Nov 2018 09:30:45 +0100
Subject: Move debug term printer to kernel

---
 vernac/himsg.ml    | 6 +++---
 vernac/ppvernac.ml | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'vernac')

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()
-- 
cgit v1.2.3