diff options
30 files changed, 77 insertions, 144 deletions
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4 index 33811b3d9..45197cf4f 100644 --- a/contrib/cc/g_congruence.ml4 +++ b/contrib/cc/g_congruence.ml4 @@ -16,14 +16,14 @@ open Tacticals (* Tactic registration *) -TACTIC EXTEND CC - [ "Congruence" ] -> [ tclORELSE +TACTIC EXTEND cc + [ "congruence" ] -> [ tclORELSE (tclTHEN (tclREPEAT introf) (cc_tactic [])) cc_fail ] END -TACTIC EXTEND CCwith - [ "Congruence" "with" ne_constr_list(l) ] -> [ tclORELSE +TACTIC EXTEND cc_with + [ "congruence" "with" ne_constr_list(l) ] -> [ tclORELSE (tclTHEN (tclREPEAT introf) (cc_tactic l)) cc_fail] END diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 index 0c35b5cda..a995f59bd 100644 --- a/contrib/extraction/g_extraction.ml4 +++ b/contrib/extraction/g_extraction.ml4 @@ -15,10 +15,7 @@ open Pcoq open Genarg open Pp -let pr_mlname _ _ _ s = - spc () ++ - (if !Options.v7 && not (Options.do_translate()) then qs s - else Pptacticnew.qsnew s) +let pr_mlname _ _ _ s = spc () ++ Pptacticnew.qsnew s ARGUMENT EXTEND mlname TYPED AS string @@ -37,21 +34,6 @@ VERNAC ARGUMENT EXTEND language | [ "Toplevel" ] -> [ Toplevel ] END -(* Temporary for translator *) -if !Options.v7 then - let pr_language _ _ _ = function - | Ocaml -> str " Ocaml" - | Haskell -> str " Haskell" - | Scheme -> str " Scheme" - | Toplevel -> str " Toplevel" - in - let globwit_language = Obj.magic rawwit_language in - let wit_language = Obj.magic rawwit_language in - Pptactic.declare_extra_genarg_pprule true - (rawwit_language, pr_language) - (globwit_language, pr_language) - (wit_language, pr_language); - (* Extraction commands *) VERNAC COMMAND EXTEND Extraction diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index e29a91959..2ee0b27ae 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -184,7 +184,7 @@ let field_term l g = (* Declaration of Field *) -TACTIC EXTEND Field -| [ "Field" ] -> [ field ] -| [ "Field" ne_constr_list(l) ] -> [ field_term l ] +TACTIC EXTEND field +| [ "field" ] -> [ field ] +| [ "field" ne_constr_list(l) ] -> [ field_term l ] END diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index 1c4ddf0be..0db32a555 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -81,23 +81,16 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) -TACTIC EXTEND Firstorder - [ "Firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> +TACTIC EXTEND firstorder + [ "firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ] -| [ "Firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> +| [ "firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ] -| [ "Firstorder" tactic_opt(t) ] -> +| [ "firstorder" tactic_opt(t) ] -> [ gen_ground_tac true (option_app eval_tactic t) Void ] END -(* Obsolete since V8.0 -TACTIC EXTEND GTauto - [ "GTauto" ] -> - [ gen_ground_tac false (Some fail_solver) Void ] -END -*) - -TACTIC EXTEND GIntuition - [ "GIntuition" tactic_opt(t) ] -> +TACTIC EXTEND gintuition + [ "gintuition" tactic_opt(t) ] -> [ gen_ground_tac false (option_app eval_tactic t) Void ] END diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index 1b96eb98c..727a03000 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -213,4 +213,4 @@ let normalize_evaluables= None->unfold_in_concl (Lazy.force defined_connectives) | Some (id,_,_)-> unfold_in_hyp (Lazy.force defined_connectives) - (id,[],(Tacexpr.InHypTypeOnly,ref None))) + (id,[],Tacexpr.InHypTypeOnly)) diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index fb75655f0..8acbe2359 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -289,9 +289,9 @@ let print_cmap map= let print_entry c l s= let xc=Constrextern.extern_constr false (Global.env ()) c in str "| " ++ - Util.prlist (Ppconstr.pr_global Idset.empty) l ++ + Util.prlist Printer.pr_global l ++ str " : " ++ - Ppconstr.pr_constr xc ++ + Ppconstrnew.pr_constr xc ++ cut () ++ s in msgnl (v 0 diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 8a546f90f..210898a14 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -281,7 +281,7 @@ let constant = Coqlib.gen_constant "Fourier" (* Standard library *) open Coqlib -let coq_sym_eqT = lazy (build_coq_sym_eqT ()) +let coq_sym_eqT = lazy (build_coq_sym_eq ()) let coq_False = lazy (build_coq_False ()) let coq_not = lazy (build_coq_not ()) let coq_eq = lazy (build_coq_eq ()) diff --git a/contrib/fourier/g_fourier.ml4 b/contrib/fourier/g_fourier.ml4 index 620cabe80..b952851fa 100644 --- a/contrib/fourier/g_fourier.ml4 +++ b/contrib/fourier/g_fourier.ml4 @@ -12,6 +12,6 @@ open FourierR -TACTIC EXTEND Fourier - [ "FourierZ" (* constr_list(l) *) ] -> [ fourier (* l *) ] +TACTIC EXTEND fourier + [ "fourierz" ] -> [ fourier ] END diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index 517e92d93..27c0658d2 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -772,8 +772,8 @@ let invfun_verif c l dorew gl = else error "wrong number of arguments for the function" -TACTIC EXTEND FunctionalInduction - [ "Functional" "Induction" constr(c) ne_constr_list(l) ] +TACTIC EXTEND functional_induction + [ "functional" "induction" constr(c) ne_constr_list(l) ] -> [ invfun_verif c l true ] END diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index ef3561a70..e2edbd8ba 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -632,17 +632,17 @@ let pcoq_hook = { } -TACTIC EXTEND Pbp -| [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> +TACTIC EXTEND pbp +| [ "pbp" ident_opt(idopt) natural_list(nl) ] -> [ if_pcoq pbp_tac_pcoq idopt nl ] END -TACTIC EXTEND CtDebugTac -| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] +TACTIC EXTEND ct_debugtac +| [ "debugtac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END -TACTIC EXTEND CtDebugTac2 -| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] +TACTIC EXTEND ct_debugtac2 +| [ "debugtac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 54508443d..b4e106a4d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -3,7 +3,6 @@ open String;; open Char;; open Util;; -open Ast;; open Names;; open Ascent;; open Genarg;; @@ -64,10 +63,6 @@ let coercion_description t = !coercion_description_holder t;; let set_coercion_description f = coercion_description_holder:=f; ();; -let string_of_node_loc the_node = - match unloc (loc the_node) with - (a,b) -> "(" ^ (string_of_int a) ^ ", " ^ (string_of_int b) ^ ")";; - let xlate_error s = failwith ("Translation error: " ^ s);; let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;; diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index 58307c334..467036e08 100644 --- a/contrib/jprover/jprover.ml4 +++ b/contrib/jprover/jprover.ml4 @@ -542,20 +542,9 @@ let jpn n gls = TCL.tclTHEN (TCL.tclTRY T.red_in_concl) (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls)) (jp n)) gls -(* -let dyn_jpn l gls = - match l with - | [PT.Integer n] -> jpn n - | _ -> jp_error "Impossible!!!" - - -let h_jp = TM.hide_tactic "Jp" dyn_jp - -let h_jpn = TM.hide_tactic "Jpn" dyn_jpn -*) -TACTIC EXTEND Jprover - [ "Jp" natural_opt(n) ] -> [ jpn n ] +TACTIC EXTEND jprover + [ "jp" natural_opt(n) ] -> [ jpn n ] END (* diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index fa6695636..5d43b1686 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -19,7 +19,6 @@ open Util open Pp open Reduction open Proof_type -open Ast open Names open Nameops open Term diff --git a/contrib/omega/g_omega.ml4 b/contrib/omega/g_omega.ml4 index 0b98a5b80..910f11083 100644 --- a/contrib/omega/g_omega.ml4 +++ b/contrib/omega/g_omega.ml4 @@ -19,6 +19,6 @@ open Coq_omega -TACTIC EXTEND Omega - [ "Omega" ] -> [ omega_solver ] +TACTIC EXTEND omega + [ "omega" ] -> [ omega_solver ] END diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 4121580ff..e67dc1fa0 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -533,8 +533,8 @@ let (value_f:constr -> global_reference -> constr) = RLambda (d0, Name x_id, RDynamic(d0, constr_in a), RCases - (d0,(None,ref None), - [RApp(d0, RRef(d0,fterm), [RVar(d0, x_id)]),ref (Anonymous,None)], + (d0,None, + [RApp(d0, RRef(d0,fterm), [RVar(d0, x_id)]),(Anonymous,None)], [d0, [v_id], [PatCstr(d0,(ind_of_ref (Lazy.force coq_sig_ref),1), [PatVar(d0, Name v_id); diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4 index e439feb8c..808cbbf27 100644 --- a/contrib/ring/g_quote.ml4 +++ b/contrib/ring/g_quote.ml4 @@ -12,7 +12,7 @@ open Quote -TACTIC EXTEND Quote - [ "Quote" ident(f) ] -> [ quote f [] ] -| [ "Quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] +TACTIC EXTEND quote + [ "quote" ident(f) ] -> [ quote f [] ] +| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] END diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4 index 9c0e5c4e7..0cb86dfdd 100644 --- a/contrib/ring/g_ring.ml4 +++ b/contrib/ring/g_ring.ml4 @@ -13,8 +13,8 @@ open Quote open Ring -TACTIC EXTEND Ring - [ "Ring" constr_list(l) ] -> [ polynom l ] +TACTIC EXTEND ring + [ "ring" constr_list(l) ] -> [ polynom l ] END (* The vernac commands "Add Ring" and co *) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 4884f23c6..5448d1389 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -835,11 +835,11 @@ let raw_polynom th op lc gl = (tclORELSE (tclORELSE (h_exact c'i_eq_c''i) - (h_exact (mkApp(build_coq_sym_eqT (), + (h_exact (mkApp(build_coq_sym_eq (), [|th.th_a; c'''i; ci; c'i_eq_c''i |])))) (tclTHENS (elim_type - (mkApp(build_coq_eqT (), [|th.th_a; c'''i; ci |]))) + (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |]))) [ tac; h_exact c'i_eq_c''i ])) ) diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 02add0dcb..fbe415707 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -492,10 +492,10 @@ Ltac elim_eq_pos t1 t2 := avec son théorème *) Theorem relation_ind2 : - forall (P : Datatypes.comparison -> Prop) (b : Datatypes.comparison), - (b = Datatypes.Eq -> P Datatypes.Eq) -> - (b = Datatypes.Lt -> P Datatypes.Lt) -> - (b = Datatypes.Gt -> P Datatypes.Gt) -> P b. + forall (P : comparison -> Prop) (b : comparison), + (b = Eq -> P Eq) -> + (b = Lt -> P Lt) -> + (b = Gt -> P Gt) -> P b. simple induction b; auto. Qed. @@ -841,31 +841,25 @@ Qed. (* \subsubsection{La tactique pour prouver la stabilité} *) Ltac loop t := - match constr:t with - | (?X1 = ?X2) => - (* Global *) - loop X1 || loop X2 + match t with + (* Global *) + | (?X1 = ?X2) => loop X1 || loop X2 | (_ -> ?X1) => loop X1 - | (interp_hyps _ _ ?X1) => - (* Interpretations *) - loop X1 + | (interp_hyps _ _ ?X1) => loop X1 | (interp_list_hyps _ _ ?X1) => loop X1 | (interp_proposition _ _ ?X1) => loop X1 | (interp_term _ ?X1) => loop X1 - | (EqTerm ?X1 ?X2) => - - (* Propositions *) - loop X1 || loop X2 + (* Propositions *) + | (EqTerm ?X1 ?X2) => loop X1 || loop X2 | (LeqTerm ?X1 ?X2) => loop X1 || loop X2 - | (?X1 + ?X2)%term => - (* Termes *) - loop X1 || loop X2 + (* Termes *) + | (?X1 + ?X2)%term => loop X1 || loop X2 | (?X1 - ?X2)%term => loop X1 || loop X2 | (?X1 * ?X2)%term => loop X1 || loop X2 | (- ?X1)%term => loop X1 - | (Tint ?X1) => - loop X1 + | (Tint ?X1) => loop X1 + (* Eliminations *) | match ?X1 with | EqTerm x x0 => _ | LeqTerm x x0 => _ @@ -881,8 +875,6 @@ Ltac loop t := | Timp x x0 => _ | Tprop x => _ end => - - (* Eliminations *) case X1; [ intro; intro | intro; intro @@ -909,9 +901,9 @@ Ltac loop t := [ intro | intro; intro | intro; intro | intro; intro | intro | intro ]; auto; Simplify | match ?X1 ?= ?X2 with - | Datatypes.Eq => _ - | Datatypes.Lt => _ - | Datatypes.Gt => _ + | Eq => _ + | Lt => _ + | Gt => _ end => elim_Zcompare X1 X2; intro; auto; Simplify | match ?X1 with @@ -1578,9 +1570,9 @@ Definition not_exact_divide (k1 k2 : Z) (body : term) with | true => match k2 ?= 0 with - | Datatypes.Gt => + | Gt => match k1 ?= k2 with - | Datatypes.Gt => absurd + | Gt => absurd | _ => l end | _ => l @@ -1613,7 +1605,7 @@ Definition contradiction (t i j : nat) (l : hyps) := | LeqTerm (Tint Z0) b2 => match fusion_cancel t (b1 + b2)%term with | Tint k => match 0 ?= k with - | Datatypes.Gt => absurd + | Gt => absurd | _ => l end | _ => l @@ -1749,7 +1741,7 @@ Definition sum (k1 k2 : Z) (trace : list t_fusion) EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | LeqTerm (Tint Z0) b2 => match k2 ?= 0 with - | Datatypes.Gt => + | Gt => LeqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | _ => TrueTerm @@ -1758,14 +1750,14 @@ Definition sum (k1 k2 : Z) (trace : list t_fusion) end | LeqTerm (Tint Z0) b1 => match k1 ?= 0 with - | Datatypes.Gt => + | Gt => match prop2 with | EqTerm (Tint Z0) b2 => LeqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | LeqTerm (Tint Z0) b2 => match k2 ?= 0 with - | Datatypes.Gt => + | Gt => LeqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term) | _ => TrueTerm @@ -1808,7 +1800,7 @@ intros a b c d; case a; case b; case c; case d; unfold Zle in |- *; simpl in |- *; auto. Qed. -Theorem sum4 : forall k : Z, (k ?= 0) = Datatypes.Gt -> 0 <= k. +Theorem sum4 : forall k : Z, (k ?= 0) = Gt -> 0 <= k. intro; case k; unfold Zle in |- *; simpl in |- *; auto; intros; discriminate. Qed. @@ -1886,9 +1878,9 @@ Definition divide_and_approx (k1 k2 : Z) (body : term) with | true => match k1 ?= 0 with - | Datatypes.Gt => + | Gt => match k1 ?= k2 with - | Datatypes.Gt => LeqTerm (Tint 0) body + | Gt => LeqTerm (Tint 0) body | _ => prop end | _ => prop diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index c8f44cf82..69b4b2def 100644 --- a/contrib/romega/const_omega.ml +++ b/contrib/romega/const_omega.ml @@ -69,7 +69,7 @@ let logic_dir = ["Coq";"Logic";"Decidable"] let coq_modules = Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] - @ [["Coq"; "Lists"; (if !Options.v7 then "PolyList" else "List")]] + @ [["Coq"; "Lists"; "List"]] @ [module_refl_path] diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4 index 386f7f287..7cfc50f8e 100644 --- a/contrib/romega/g_romega.ml4 +++ b/contrib/romega/g_romega.ml4 @@ -10,6 +10,6 @@ open Refl_omega -TACTIC EXTEND ROmega - [ "ROmega" ] -> [ total_reflexive_omega_tactic ] +TACTIC EXTEND romelga + [ "romega" ] -> [ total_reflexive_omega_tactic ] END diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index eb372b5b8..5a7e8afd5 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -1308,7 +1308,6 @@ let resolution env full_reified_goal systems_list = Tactics.apply (Lazy.force coq_I) let total_reflexive_omega_tactic gl = - if !Options.v7 then Util.error "ROmega does not work in v7 mode"; Coqlib.check_required_library ["Coq";"romega";"ROmega"]; try let env = new_environment () in diff --git a/contrib/rtauto/g_rtauto.ml4 b/contrib/rtauto/g_rtauto.ml4 index ee47d0b02..4cbe84368 100644 --- a/contrib/rtauto/g_rtauto.ml4 +++ b/contrib/rtauto/g_rtauto.ml4 @@ -10,7 +10,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -TACTIC EXTEND Rtauto - [ "Rtauto" ] -> [ Refl_tauto.rtauto_tac ] +TACTIC EXTEND rtauto + [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ] END diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 6a78e88c7..d965e39c2 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -198,7 +198,7 @@ let protect_tac = Tactics.reduct_option (protect_red,DEFAULTcast) None ;; let protect_tac_in id = - Tactics.reduct_option (protect_red,DEFAULTcast) (Some(id,[],(InHyp, ref None)));; + Tactics.reduct_option (protect_red,DEFAULTcast) (Some(id,[],InHyp));; TACTIC EXTEND protect_fv diff --git a/contrib/subtac/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4 index 7b4bc31b4..095e5fafc 100644 --- a/contrib/subtac/g_eterm.ml4 +++ b/contrib/subtac/g_eterm.ml4 @@ -19,8 +19,8 @@ open Eterm -TACTIC EXTEND Eterm - [ "Eterm" ] -> [ +TACTIC EXTEND eterm + [ "eterm" ] -> [ (fun gl -> let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in Eterm.etermtac (evm, t) gl) ] diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4 index 229c308a4..dbb149c20 100644 --- a/contrib/subtac/sparser.ml4 +++ b/contrib/subtac/sparser.ml4 @@ -83,9 +83,7 @@ end open Subtac open Util -open Coqast -if not !Options.v7 then GEXTEND Gram GLOBAL: subtac_spec subtac_term subtac_wf_proof_type; @@ -231,7 +229,6 @@ GEXTEND Gram ] ; END -else (* Developped with Coq 8.0 *) () type type_loc_argtype = (type_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type type term_loc_argtype = (term_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index b9d920903..698c732d2 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 = if !Options.v7 then Pptactic.pr_tactic else Pptacticnew.pr_tactic (Global.env()) in + let prtac = Pptacticnew.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 @@ -11,9 +11,6 @@ install_printer Top_printers.prkn install_printer Top_printers.prcon install_printer Top_printers.prsp install_printer Top_printers.prqualid -install_printer Top_printers.prast -install_printer Top_printers.prastpat -install_printer Top_printers.prastpatl install_printer Top_printers.ppbigint install_printer Top_printers.pppattern diff --git a/dev/include b/dev/include index eabf79a48..d1b5a717b 100644 --- a/dev/include +++ b/dev/include @@ -4,10 +4,6 @@ #cd ".";; #use "base_include";; -#install_printer (* ast *) prast;; -#install_printer (* pat *) prastpat;; -#install_printer (* patlist *) prastpatl;; - #install_printer (* pattern *) pppattern;; #install_printer (* rawconstr *) pprawterm;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e8dffb437..6a3c19c5f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -10,7 +10,6 @@ open System open Pp -open Ast open Names open Libnames open Nameops @@ -54,11 +53,6 @@ let ppbigint n = pp (Bigint.pr_bigint n);; let pP s = pp (hov 0 s) -let prast c = pp(print_ast c) - -let prastpat c = pp(print_astpat c) -let prastpatl c = pp(print_astlpat c) - let safe_prglobal = function | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ @@ -107,7 +101,7 @@ let ppenv e = pp (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e (rel_context e) ++ str "]") -let pptac = (fun x -> pp(Pptactic.pr_glob_tactic x)) +let pptac = (fun x -> pp(Pptacticnew.pr_glob_tactic (Global.env()) x)) let pr_obj obj = Format.print_string (Libobject.object_tag obj) |