diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /parsing/pptactic.mli | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'parsing/pptactic.mli')
-rw-r--r-- | parsing/pptactic.mli | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 40880f58..0f82071d 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -1,20 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pptactic.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pp open Genarg open Tacexpr open Pretyping open Proof_type open Topconstr -open Rawterm +open Glob_term open Pattern open Ppextend open Environ @@ -32,8 +30,8 @@ type 'a raw_extra_genarg_printer = 'a -> std_ppcmds type 'a glob_extra_genarg_printer = - (rawconstr_and_expr -> std_ppcmds) -> - (rawconstr_and_expr -> std_ppcmds) -> + (glob_constr_and_expr -> std_ppcmds) -> + (glob_constr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -43,7 +41,7 @@ type 'a extra_genarg_printer = (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds - (* if the boolean is false then the extension applies only to old syntax *) + (** if the boolean is false then the extension applies only to old syntax *) val declare_extra_genarg_pprule : ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) -> ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> @@ -51,7 +49,7 @@ val declare_extra_genarg_pprule : type grammar_terminals = string option list - (* if the boolean is false then the extension applies only to old syntax *) + (** if the boolean is false then the extension applies only to old syntax *) val declare_extra_tactic_pprule : string * argument_type list * (int * grammar_terminals) -> unit @@ -72,9 +70,9 @@ val pr_raw_extend: string -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: - (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) -> + (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (rawconstr_pattern_and_expr -> std_ppcmds) -> int -> + (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> string -> glob_generic_argument list -> std_ppcmds val pr_extend : |