diff options
| author | herbelin | 2005-01-21 17:18:23 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-21 17:18:23 +0000 |
| commit | d7b2414b631d71e89e677d650b84bd4fadd44895 (patch) | |
| tree | 47b653e7e0ae9b83dbc8a96b2c5be4717b2eefbd /parsing | |
| parent | ea6bd4e5496f0fd7e059cd9b924f29ca80a38ae2 (diff) | |
Compatibilité ocamlweb pour cible doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/coqast.mli | 4 | ||||
| -rw-r--r-- | parsing/esyntax.mli | 11 | ||||
| -rw-r--r-- | parsing/extend.mli | 5 | ||||
| -rw-r--r-- | parsing/printer.mli | 3 |
4 files changed, 2 insertions, 21 deletions
diff --git a/parsing/coqast.mli b/parsing/coqast.mli index b588d9cea0..a083d09a68 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -42,9 +42,9 @@ val hcons_ast: * (kernel_name -> kernel_name) * (constant -> constant) -> (t -> t) * (loc -> loc) -(* +(*i val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr val fold_tactic_expr : ('a -> t -> 'a) -> ('a -> tactic_expr -> 'a) -> 'a -> tactic_expr -> 'a val iter_tactic_expr : (tactic_expr -> unit) -> tactic_expr -> unit -*) +i*) diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli index d6a7f44689..0344a27e2e 100644 --- a/parsing/esyntax.mli +++ b/parsing/esyntax.mli @@ -48,16 +48,5 @@ module Ppprim : val declare_primitive_printer : string -> scope_name -> primitive_printer -> unit -(* -val declare_infix_symbol : Libnames.section_path -> string -> unit -*) - (* Generic printing functions *) -(* -val token_printer: std_printer -> std_printer -*) -(* -val print_syntax_entry : - string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds -*) val genprint : std_printer -> unparsing_subfunction diff --git a/parsing/extend.mli b/parsing/extend.mli index c9558a970c..80a0e44487 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -113,11 +113,6 @@ type 'pat unparsing_hunk = | UNP_FNL | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk -(*val subst_unparsing_hunk : - substitution -> (substitution -> 'pat -> 'pat) -> - 'pat unparsing_hunk -> 'pat unparsing_hunk -*) - (* Checks if the precedence of the parent printer (None means the highest precedence), and the child's one, follow the given relation. *) diff --git a/parsing/printer.mli b/parsing/printer.mli index 01b691a13a..8be938f815 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -24,9 +24,6 @@ open Proof_type (*i*) (* These are the entry points for printing terms, context, tac, ... *) -(* -val gentacpr : Tacexpr.raw_tactic_expr -> std_ppcmds -*) val prterm_env : env -> constr -> std_ppcmds val prterm_env_at_top : env -> constr -> std_ppcmds |