diff options
| -rw-r--r-- | dev/top_printers.ml | 7 | ||||
| -rw-r--r-- | parsing/termast.ml | 9 | ||||
| -rw-r--r-- | parsing/termast.mli | 3 |
3 files changed, 12 insertions, 7 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 321a095d0..ac5e3d0c8 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -26,7 +26,7 @@ open Termops open Clenv open Cerrors -let _ = Termast.print_evar_arguments := true +let _ = Constrextern.print_evar_arguments := true let pP s = pp (hov 0 s) @@ -35,7 +35,7 @@ let prast c = pp(print_ast c) let prastpat c = pp(print_astpat c) let prastpatl c = pp(print_astlpat c) let ppterm x = pp(prterm x) -let ppterm_univ x = Termast.with_universes ppterm x +let ppterm_univ x = Constrextern.with_universes ppterm x let pprawterm = (fun x -> pp(pr_rawterm x)) let pppattern = (fun x -> pp(pr_pattern x)) let pptype = (fun x -> pp(prtype x)) @@ -63,8 +63,7 @@ let prconst (sp,j) = let prvar ((id,a)) = pp (str"#" ++ pr_id id ++ str":" ++ prterm a) -let genprj f j = - let (c,t) = Termast.with_casts f j in (c ++ str " : " ++ t) +let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t) let prj j = pp (genprj prjudge j) diff --git a/parsing/termast.ml b/parsing/termast.ml index f1ce602fb..8405c6cf1 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -31,24 +31,29 @@ open Nametab (**********************************************************************) (* Parametrization *) - +open Constrextern +(* (* This governs printing of local context of references *) let print_arguments = ref false (* If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false +*) (* This forces printing of cast nodes *) let print_casts = ref true +(* (* This governs printing of implicit arguments. When [print_implicits] is on then [print_implicits_explicit_args] tells how implicit args are printed. If on, implicit args are printed prefixed by "!" otherwise the function and not the arguments is prefixed by "!" *) let print_implicits = ref false +*) let print_implicits_explicit_args = ref false +(* (* This forces printing of coercions *) let print_coercions = ref false @@ -66,7 +71,7 @@ let with_casts f = with_option print_casts f let with_implicits f = with_option print_implicits f let with_coercions f = with_option print_coercions f let with_universes f = with_option print_universes f - +*) (**********************************************************************) (* conversion of references *) diff --git a/parsing/termast.mli b/parsing/termast.mli index c6e94fe16..9b87af5f8 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -39,7 +39,7 @@ val ast_of_inductive : env -> inductive -> Coqast.t val ast_of_ref : global_reference -> Coqast.t val ast_of_qualid : qualid -> Coqast.t -(* For debugging *) +(*i Now in constrextern.mli val print_implicits : bool ref val print_casts : bool ref val print_arguments : bool ref @@ -52,3 +52,4 @@ val with_implicits : ('a -> 'b) -> 'a -> 'b val with_arguments : ('a -> 'b) -> 'a -> 'b val with_coercions : ('a -> 'b) -> 'a -> 'b val with_universes : ('a -> 'b) -> 'a -> 'b +i*) |