aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/psyntax.ml414
-rw-r--r--contrib/dp/dp.ml2
-rw-r--r--contrib/extraction/g_extraction.ml42
-rw-r--r--contrib/field/field.ml42
-rw-r--r--contrib/first-order/sequent.ml2
-rwxr-xr-xcontrib/interface/blast.ml2
-rw-r--r--contrib/interface/centaur.ml42
-rw-r--r--contrib/interface/debug_tac.ml42
-rw-r--r--contrib/interface/xlate.ml7
-rw-r--r--contrib/setoid_ring/newring.ml42
-rw-r--r--contrib/subtac/infer.ml2
-rw-r--r--contrib/subtac/rewrite.ml2
-rw-r--r--contrib/xml/proofTree2Xml.ml42
13 files changed, 21 insertions, 22 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 22c7e204a..ece466849 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -852,7 +852,7 @@ let pr_effects x =
let (ro,rw) = Peffect.get_repr x in pr_reads ro ++ pr_writes rw
let pr_predicate delimited { a_name = n; a_value = c } =
- (if delimited then Ppconstrnew.pr_lconstr else Ppconstrnew.pr_constr) c ++
+ (if delimited then Ppconstr.pr_lconstr else Ppconstr.pr_constr) c ++
(match n with Name id -> spc () ++ str "as " ++ pr_id id | Anonymous -> mt())
let pr_assert b { p_name = x; p_value = v } =
@@ -870,7 +870,7 @@ let pr_post_condition_opt = function
let rec pr_type_v_v8 = function
| Array (a,v) ->
- str "array" ++ spc() ++ Ppconstrnew.pr_constr a ++ spc() ++ str "of " ++
+ str "array" ++ spc() ++ Ppconstr.pr_constr a ++ spc() ++ str "of " ++
pr_type_v_v8 v
| v -> pr_type_v3 v
@@ -882,7 +882,7 @@ and pr_type_v3 = function
pr_type_v_v8 v ++ pr_effects e ++
pr_pre_condition_list prel ++ pr_post_condition_opt postl ++
spc () ++ str "end"
- | TypePure a -> Ppconstrnew.pr_constr a
+ | TypePure a -> Ppconstr.pr_constr a
| v -> str "(" ++ pr_type_v_v8 v ++ str ")"
and pr_binder = function
@@ -910,9 +910,9 @@ let pr_invariant = function
| Some c -> hov 2 (str "invariant" ++ spc () ++ pr_predicate false c)
let pr_variant (c1,c2) =
- Ppconstrnew.pr_constr c1 ++
+ Ppconstr.pr_constr c1 ++
(try Constrextern.check_same_type c2 (ast_zwf_zero dummy_loc); mt ()
- with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstrnew.pr_constr c2))
+ with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstr.pr_constr c2))
let rec pr_desc = function
| Variable id ->
@@ -1025,7 +1025,7 @@ let rec pr_desc = function
(* Numeral or "tt": use a printer which doesn't globalize *)
Ppconstr.pr_constr
(Constrextern.extern_constr_in_scope false "Z_scope" (Global.env()) c)
- | Debug (s,p) -> str "@" ++ Pptacticnew.qsnew s ++ pr_prog p
+ | Debug (s,p) -> str "@" ++ Pptactic.qsnew s ++ pr_prog p
and pr_block_st = function
| Label s -> hov 0 (str "label" ++ spc() ++ str s)
@@ -1046,7 +1046,7 @@ and pr_prog0 b { desc = desc; pre = pre; post = post } =
hov 0
(if b & post<>None then str"(" ++ pr_desc desc ++ str")"
else pr_desc desc)
- ++ Ppconstrnew.pr_opt pr_postcondition post)
+ ++ Ppconstr.pr_opt pr_postcondition post)
and pr_prog x = pr_prog0 true x
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index b2669d317..f25794e80 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -172,7 +172,7 @@ let rec_names_for c =
| Name id ->
let c' = Names.make_con mp dp (label_of_id id) in
ignore (Global.lookup_constant c');
- msgnl (Ppconstrnew.pr_term (mkConst c'));
+ msgnl (Ppconstr.pr_term (mkConst c'));
c'
| Anonymous ->
raise Not_found)
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index a995f59bd..c615e80fa 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -15,7 +15,7 @@ open Pcoq
open Genarg
open Pp
-let pr_mlname _ _ _ s = spc () ++ Pptacticnew.qsnew s
+let pr_mlname _ _ _ s = spc () ++ Pptactic.qsnew s
ARGUMENT EXTEND mlname
TYPED AS string
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 2ee0b27ae..f0a5489df 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -114,7 +114,7 @@ END
*)
(* For the translator, otherwise the code above is OK *)
-open Ppconstrnew
+open Ppconstr
let pp_minus_div_arg _prc _prlc _prt (omin,odiv) =
if omin=None && odiv=None then mt() else
spc() ++ str "with" ++
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 8acbe2359..f9ebafc2a 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -291,7 +291,7 @@ let print_cmap map=
str "| " ++
Util.prlist Printer.pr_global l ++
str " : " ++
- Ppconstrnew.pr_constr xc ++
+ Ppconstr.pr_constr xc ++
cut () ++
s in
msgnl (v 0
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 78716435c..f7f6674e8 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -595,7 +595,7 @@ let blast_tac display_function = function
let blast_tac_txt =
blast_tac
- (function x -> msgnl(Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));;
+ (function x -> msgnl(Pptactic.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));;
(* Obsolète ?
overwriting_add_tactic "Blast1" blast_tac_txt;;
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 80dc1a40f..e79d14249 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -346,7 +346,7 @@ let debug_tac2_pcoq tac =
(errorlabstrm "DEBUG TACTIC"
(str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++
fnl () ++ str "the tactic is" ++ fnl () ++
- Pptacticnew.pr_glob_tactic (Global.env()) tac);
+ Pptactic.pr_glob_tactic (Global.env()) tac);
result)
with
e ->
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index a7ea5ea62..dbb85895a 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -10,7 +10,7 @@ open Proof_type;;
open Tacexpr;;
open Genarg;;
-let pr_glob_tactic = Pptacticnew.pr_glob_tactic (Global.env())
+let pr_glob_tactic = Pptactic.pr_glob_tactic (Global.env())
(* Compacting and uncompacting proof commands *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 1439d4cd1..f0e9c120b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -416,7 +416,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
let strip_mutrec (fid, n, bl, arf, ardef) =
let (struct_arg,bl,arf,ardef) =
if bl = [] then
- let (bl,arf,ardef) = Ppconstrnew.split_fix (n+1) arf ardef in
+ let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
@@ -1785,8 +1785,7 @@ let rec xlate_vernac =
xlate_error "TODO: Print Canonical Structures"
| PrintInspect n -> CT_inspect (CT_int n)
| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
- | PrintLocalContext -> CT_print
- | PrintSetoids -> CT_print_setoids
+ | PrintSetoids -> CT_print_setoids
| PrintTables -> CT_print_tables
| PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
| PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
@@ -1870,7 +1869,7 @@ let rec xlate_vernac =
let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
let (struct_arg,bl,arf,ardef) =
if bl = [] then
- let (bl,arf,ardef) = Ppconstrnew.split_fix (n+1) arf ardef in
+ let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index d965e39c2..2facb0dcb 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -27,7 +27,7 @@ open Setoid_replace
open Proof_type
open Coqlib
open Tacmach
-open Ppconstrnew
+open Ppconstr
open Mod_subst
open Tacinterp
open Libobject
diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml
index 876dc68bb..987fbedda 100644
--- a/contrib/subtac/infer.ml
+++ b/contrib/subtac/infer.ml
@@ -6,7 +6,7 @@ open Util
open Sast
open Scoq
open Pp
-open Ppconstrnew
+open Ppconstr
let ($) f g = fun x -> f (g x)
diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
index ce0f15ec2..b228be2a7 100644
--- a/contrib/subtac/rewrite.ml
+++ b/contrib/subtac/rewrite.ml
@@ -7,7 +7,7 @@ open Term
open Names
open Scoq
open Pp
-open Ppconstrnew
+open Ppconstr
open Util
type recursion_info = {
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 698c732d2..1de6a4325 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -156,7 +156,7 @@ Pp.ppnl (Pp.(++) (Pp.str
aux flat_proof old_hyps
| _ ->
(****** la tactique employee *)
- let prtac = Pptacticnew.pr_tactic (Global.env()) in
+ let prtac = Pptactic.pr_tactic (Global.env()) in
let tac = std_ppcmds_to_string (prtac tactic_expr) in
let tacname= first_word tac in
let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 19:47:10 +0000