diff options
| author | filliatr | 2000-01-27 23:09:26 +0000 |
|---|---|---|
| committer | filliatr | 2000-01-27 23:09:26 +0000 |
| commit | bd23886243736ba75a584c475b7da521571c646d (patch) | |
| tree | 26c93a33ee1f4e02bad47c13682998a6c554765f /kernel | |
| parent | 5771e5cd2cb76e0c8a05481417e12921da06c8ca (diff) | |
erreurs latex dans interfaces
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@287 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.mli | 26 | ||||
| -rw-r--r-- | kernel/sign.mli | 2 |
2 files changed, 15 insertions, 13 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c28d35c8d6..2b68faa0c8 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -63,20 +63,22 @@ val mis_consnames : mind_specif -> identifier array val mind_nth_type_packet : mutual_inductive_body -> int -> mutual_inductive_packet -(* A light version of mind_specif_of_mind with pre-splitted args +(* A light version of [mind_specif_of_mind] with pre-splitted args Invariant: We have - -- Hnf (fullmind) = DOPN(AppL,[|MutInd mind;..params..;..realargs..|]) - -- with mind = ((sp,i),localvars) for some sp, i, localvars + + -- [Hnf (fullmind)] = [DOPN(AppL,[|MutInd mind;..params..;..realargs..|])] + + with [mind] = [((sp,i),localvars)] for some [sp, i, localvars] *) -type inductive_summary = - {fullmind : constr; - mind : inductive; - nparams : int; - nrealargs : int; - nconstr : int; - params : constr list; - realargs : constr list; - arity : constr} +type inductive_summary = { + fullmind : constr; + mind : inductive; + nparams : int; + nrealargs : int; + nconstr : int; + params : constr list; + realargs : constr list; + arity : constr } (*s Declaration of inductive types. *) diff --git a/kernel/sign.mli b/kernel/sign.mli index fa05df814a..3a8f8a47a5 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -78,7 +78,7 @@ val ids_of_env : ('a, 'b) sign -> identifier list val number_of_rels : ('b,'a) sign -> int (*i This is for Cases i*) -(* raise Not_found if the integer is out of range *) +(* raise [Not_found] if the integer is out of range *) val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign type ('b,'a) search_result = |