diff options
Diffstat (limited to 'interp/genarg.mli')
| -rw-r--r-- | interp/genarg.mli | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/interp/genarg.mli b/interp/genarg.mli index fab5ff33e..50abd351e 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) @@ -26,9 +26,9 @@ type 'a or_by_notation = val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc -(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) -(* in the environment by the effective calls to Intro, Inversion, etc *) -(* The [constr_expr] field is [None] in TacDef though *) +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) type rawconstr_and_expr = rawconstr * constr_expr option type open_constr_expr = unit * constr_expr @@ -51,9 +51,9 @@ and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds -(* The route of a generic argument, from parsing to evaluation +(** The route of a generic argument, from parsing to evaluation -\begin{verbatim} +{% \begin{%}verbatim{% }%} parsing in_raw out_raw char stream ----> rawtype ----> constr_expr generic_argument --------| encapsulation decaps | @@ -76,7 +76,7 @@ val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds | V effective use -\end{verbatim} +{% \end{%}verbatim{% }%} To distinguish between the uninterpreted (raw), globalized and interpreted worlds, we annotate the type [generic_argument] by a @@ -84,7 +84,7 @@ phantom argument which is either [constr_expr], [rawconstr] or [constr]. Transformation for each type : -\begin{verbatim} +{% \begin{%}verbatim{% }%} tag raw open type cooked closed type BoolArgType bool bool @@ -107,10 +107,10 @@ List0ArgType of argument_type List1ArgType of argument_type OptArgType of argument_type ExtraArgType of string '_a '_b -\end{verbatim} +{% \end{%}verbatim{% }%} *) -(* All of [rlevel], [glevel] and [tlevel] must be non convertible +(** All of [rlevel], [glevel] and [tlevel] must be non convertible to ensure the injectivity of the type inference from type ['co generic_argument] to [('a,'co) abstract_argument_type]; this guarantees that, for 'co fixed, the type of @@ -222,7 +222,7 @@ val wit_pair : ('b,'co) abstract_argument_type -> ('a * 'b,'co) abstract_argument_type -(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) +(** ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) type 'a generic_argument val fold_list0 : @@ -238,7 +238,7 @@ val fold_pair : ('a generic_argument -> 'a generic_argument -> 'c) -> 'a generic_argument -> 'c -(* [app_list0] fails if applied to an argument not of tag [List0 t] +(** [app_list0] fails if applied to an argument not of tag [List0 t] for some [t]; it's the responsability of the caller to ensure it *) val app_list0 : ('a generic_argument -> 'b generic_argument) -> @@ -255,7 +255,7 @@ val app_pair : ('a generic_argument -> 'b generic_argument) -> 'a generic_argument -> 'b generic_argument -(* create a new generic type of argument: force to associate +(** create a new generic type of argument: force to associate unique ML types at each of the three levels *) val create_arg : string -> ('a,tlevel) abstract_argument_type @@ -265,7 +265,7 @@ val create_arg : string -> val exists_argtype : string -> bool type argument_type = - (* Basic types *) + (** Basic types *) | BoolArgType | IntArgType | IntOrVarArgType @@ -275,7 +275,7 @@ type argument_type = | IdentArgType of bool | VarArgType | RefArgType - (* Specific types *) + (** Specific types *) | SortArgType | ConstrArgType | ConstrMayEvalArgType @@ -300,7 +300,7 @@ val out_gen : ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a -(* [in_generic] is used in combination with camlp4 [Gramext.action] magic +(** [in_generic] is used in combination with camlp4 [Gramext.action] magic [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument] |