diff options
| author | herbelin | 2005-12-26 20:07:21 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-26 20:07:21 +0000 |
| commit | 52f4136ecf452162adb55c8de031b73c97dcdbac (patch) | |
| tree | 8ac0a4c3584025a44067c6a96c6ce9d92ca93e78 /toplevel | |
| parent | 099fb1b4c5084bb899e4910e42c971cdfa81e1aa (diff) | |
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
4 files changed, 2 insertions, 8 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f74d7efc82..6e72dd63a3 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -272,10 +272,6 @@ let parse_args is_ide = | "-no-hash-consing" :: rem -> Options.hash_cons_proofs := false; parse rem - (* Translator options *) - | "-strict-implicit" :: rem -> - Options.translate_strict_impargs := false; parse rem - | s :: rem -> if is_ide then begin ide_args := s :: !ide_args; diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9232584cc2..8a2cb41759 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -17,7 +17,7 @@ open Options open System open Vernacexpr open Vernacinterp -open Ppvernacnew +open Ppvernac (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions @@ -132,7 +132,7 @@ let post_printing loc (env,t,f,n) = function | VernacSolve (i,_,deftac) -> let loc = unloc loc in set_formatter_translator(); - let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in + let pp = Ppvernac.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in (if !translate_file then begin msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1))); end diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4be7c93056..6cc72c0567 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -852,7 +852,6 @@ let vernac_global_check c = let vernac_print = function | PrintTables -> print_tables () - | PrintLocalContext -> msg (print_local_context ()) | PrintFullContext -> msg (print_full_context_typ ()) | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index a0ea22413e..36a0d237d2 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -34,7 +34,6 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference type printable = | PrintTables - | PrintLocalContext | PrintFullContext | PrintSectionContext of reference | PrintInspect of int |