From d7b2414b631d71e89e677d650b84bd4fadd44895 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 21 Jan 2005 17:18:23 +0000 Subject: Compatibilité ocamlweb pour cible doc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrextern.mli | 2 +- interp/constrintern.mli | 4 ++-- interp/coqlib.mli | 4 ++-- interp/genarg.mli | 24 ++++++++++++++---------- interp/notation.mli | 14 +++++++------- interp/ppextend.mli | 2 +- interp/topconstr.mli | 8 ++++---- 7 files changed, 31 insertions(+), 27 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 71127a92d..059b13c57 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ *) +(*i $Id$ i*) (*i*) open Util diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4ff60578a..03ad950c7 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ *) +(*i $Id$ i*) (*i*) open Names @@ -64,7 +64,7 @@ val interp_casted_openconstr : (* [interp_type_with_implicits] extends [interp_type] by allowing implicits arguments in the ``rel'' part of [env]; the extra argument associates a list of implicit positions to identifiers - declared in the rel_context of [env] *) + declared in the [rel_context] of [env] *) val interp_type_with_implicits : evar_map -> env -> full_implicits_env -> constr_expr -> types diff --git a/interp/coqlib.mli b/interp/coqlib.mli index fb4b2a423..6741e1a0a 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names @@ -80,7 +80,7 @@ val build_coq_eq_data : coq_leibniz_eq_data delayed val build_coq_eqT_data : coq_leibniz_eq_data delayed val build_coq_idT_data : coq_leibniz_eq_data delayed -val build_coq_eq : constr delayed (* = (build_coq_eq_data()).eq *) +val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *) val build_coq_f_equal2 : constr delayed val build_coq_eqT : constr delayed val build_coq_sym_eqT : constr delayed diff --git a/interp/genarg.mli b/interp/genarg.mli index af02a9ebe..042520151 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Util open Names @@ -19,9 +19,9 @@ open Term type 'a or_var = ArgArg of 'a | ArgVar of identifier located type 'a and_short_name = 'a * identifier located option -(* In globalize tactics, we need to keep the initial constr_expr to recompute*) +(* 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 *) +(* The [constr_expr] field is [None] in TacDef though *) type rawconstr_and_expr = rawconstr * constr_expr option type open_constr = Evd.evar_map * Term.constr @@ -39,6 +39,7 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds (* The route of a generic argument, from parsing to evaluation +\begin{verbatim} parsing in_raw out_raw char stream ----> rawtype ----> rawconstr generic_argument ----> | @@ -46,16 +47,18 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds V type <---- constr generic_argument <---- out in +\end{verbatim} To distinguish between the uninterpreted (raw) and the interpreted -worlds, we annotate the type generic_argument by a phantom argument -which is either constr_expr or constr (actually we add also a second -argument raw_tactic_expr and tactic, but this is only for technical +worlds, we annotate the type [generic_argument] by a phantom argument +which is either [constr_expr] or [constr] (actually we add also a second +argument [raw_tactic_expr] and [tactic], but this is only for technical reasons, because these types are undefined at the type of compilation -of Genarg). +of [Genarg]). Transformation for each type : -tag f raw open type cooked closed type +\begin{verbatim} +tag raw open type cooked closed type BoolArgType bool bool IntArgType int int @@ -76,6 +79,7 @@ List0ArgType of argument_type List1ArgType of argument_type OptArgType of argument_type ExtraArgType of string '_a '_b +\end{verbatim} *) type ('a,'co,'ta) abstract_argument_type @@ -175,7 +179,7 @@ val wit_pair : ('b,'co,'ta) abstract_argument_type -> ('a * 'b,'co,'ta) abstract_argument_type -(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *) +(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) type ('a,'b) generic_argument val fold_list0 : @@ -255,7 +259,7 @@ val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a| - in_generic is not typable; we replace the second argument by an absurd + [in_generic] is not typable; we replace the second argument by an absurd type (with no introduction rule) *) type an_arg_of_this_type diff --git a/interp/notation.mli b/interp/notation.mli index e803d65e7..0e401acd6 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Util @@ -30,7 +30,7 @@ open Ppextend type level = precedence * tolerability list type delimiters = string type scope -type scopes (* = scope_name list*) +type scopes (* = [scope_name list] *) val type_scope : scope_name val declare_scope : scope_name -> unit @@ -52,7 +52,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name (*s Declare and uses back and forth a numeral interpretation *) -(* A numeral interpreter is the pair of an interpreter for _integer_ +(* A numeral interpreter is the pair of an interpreter for **integer** numbers in terms and an optional interpreter in pattern, if negative numbers are not supported, the interpreter must fail with an appropriate error message *) @@ -69,12 +69,12 @@ type required_module = global_reference * string list val declare_numeral_interpreter : scope_name -> required_module -> num_interpreter -> num_uninterpreter -> unit -(* Returns the term/cases_pattern bound to a numeral in a given scope context*) +(* Return the [term]/[cases_pattern] bound to a numeral in a given scope context*) val interp_numeral : loc -> bigint -> scope_name list -> rawconstr val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list -> cases_pattern -(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *) +(* Return the numeral bound to a [term]/[cases_pattern]; raise [No_match] if no *) (* such numeral *) val uninterp_numeral : rawconstr -> scope_name * bigint val uninterp_cases_numeral : cases_pattern -> scope_name * bigint @@ -92,11 +92,11 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit -(* Returns the interpretation bound to a notation *) +(* Return the interpretation bound to a notation *) val interp_notation : loc -> notation -> scope_name list -> interpretation * ((dir_path * string) * scope_name option) -(* Returns the possible notations for a given term *) +(* Return the possible notations for a given term *) val uninterp_notations : rawconstr -> (interp_rule * interpretation * int option) list val uninterp_cases_pattern_notations : cases_pattern -> diff --git a/interp/ppextend.mli b/interp/ppextend.mli index 68927dbad..bddd1eef2 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 4cfa0a0da..51fcd9c07 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp @@ -24,12 +24,12 @@ open Mod_subst (* non global expressions such as existential variables also *) type aconstr = - (* Part common to rawconstr and cases_pattern *) + (* Part common to [rawconstr] and [cases_pattern] *) | ARef of global_reference | AVar of identifier | AApp of aconstr * aconstr list | AList of identifier * identifier * aconstr * aconstr * bool - (* Part only in rawconstr *) + (* Part only in [rawconstr] *) | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr @@ -60,7 +60,7 @@ type scope_name = string type interpretation = (identifier * (scope_name option * scope_name list)) list * aconstr -val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation -> +val match_aconstr : rawconstr -> interpretation -> (rawconstr * (scope_name option * scope_name list)) list (*s Concrete syntax for terms *) -- cgit v1.2.3