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 --- pretyping/clenv.mli | 8 ++++---- pretyping/inductiveops.mli | 4 ++-- pretyping/matching.mli | 2 +- pretyping/rawterm.mli | 4 ++-- pretyping/tacred.mli | 2 +- pretyping/termops.mli | 5 ++--- 6 files changed, 12 insertions(+), 13 deletions(-) (limited to 'pretyping') diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 3208bd593..2e8057cb0 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -36,7 +36,7 @@ type clausenv = { templval : constr freelisted; templtyp : constr freelisted } -(* Substitution is not applied on templenv (because subst_clenv is +(* Substitution is not applied on templenv (because [subst_clenv] is applied only on hints which typing env is overwritten by the goal env) *) val subst_clenv : substitution -> clausenv -> clausenv @@ -47,7 +47,7 @@ val clenv_value : clausenv -> constr val clenv_type : clausenv -> types (* substitute resolved metas *) val clenv_nf_meta : clausenv -> constr -> constr -(* type of a meta in clenvś context *) +(* type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types val mk_clenv_from : evar_info sigma -> constr * types -> clausenv @@ -67,7 +67,7 @@ val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv (***************************************************************) (* Unification with clenvs *) -(* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *) +(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) val clenv_unify : bool -> conv_pb -> constr -> constr -> clausenv -> clausenv @@ -75,7 +75,7 @@ val clenv_unify : val clenv_unique_resolver : bool -> clausenv -> evar_info sigma -> clausenv -(* same as above (allow_K=false) but replaces remaining metas +(* same as above ([allow_K=false]) but replaces remaining metas with fresh evars *) val evar_clenv_unique_resolver : clausenv -> evar_info sigma -> clausenv diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 2bc813678..7f18a7943 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Names open Term @@ -77,7 +77,7 @@ val make_arity_signature : val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types -(* Raise Not_found if not given an valid inductive type *) +(* Raise [Not_found] if not given an valid inductive type *) val extract_mrectype : constr -> inductive * constr list val find_mrectype : env -> evar_map -> constr -> inductive * constr list val find_rectype : env -> evar_map -> constr -> inductive_type diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 2b0b8f240..b4f6c3245 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -40,7 +40,7 @@ val is_matching : constr_pattern -> constr -> bool val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (* [match_subterm n pat c] returns the substitution and the context - corresponding to the [n+1]th _closed_ subterm of [c] matching [pat]; + corresponding to the [n+1]th **closed** subterm of [c] matching [pat]; It raises PatternMatchingFailure if no such matching exists *) val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 759e0adb6..b56e862ac 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -89,11 +89,11 @@ i*) val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr -(* +(*i val map_rawconstr_with_binders_loc : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr -*) +i*) val occur_rawconstr : identifier -> rawconstr -> bool diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index b7d8c1b85..423a04723 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -65,7 +65,7 @@ val reduce_to_atomic_ind : env -> evar_map -> types -> inductive * types val reduce_to_quantified_ind : env -> evar_map -> types -> inductive * types (* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form - [t'=(x1:A1)..(xn:An)(ref args)] and raise Not_found if not possible *) + [t'=(x1:A1)..(xn:An)(ref args)] and raise [Not_found] if not possible *) val reduce_to_quantified_ref : env -> evar_map -> Libnames.global_reference -> types -> types diff --git a/pretyping/termops.mli b/pretyping/termops.mli index adc0e6daa..b290a5e5f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Util open Pp @@ -16,7 +16,6 @@ open Sign open Environ (* Universes *) -(*val set_module : Names.dir_path -> unit*) val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts val new_Type : unit -> types @@ -139,7 +138,7 @@ val named_hd_type : env -> types -> name -> name val mkProd_name : env -> name * types * types -> types val mkLambda_name : env -> name * types * constr -> constr -(* Deprecated synonyms of mkProd_name and mkLambda_name *) +(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *) val prod_name : env -> name * types * types -> types val lambda_name : env -> name * types * constr -> constr -- cgit v1.2.3