diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 2 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.mli | 2 | ||||
| -rw-r--r-- | kernel/retroknowledge.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 894f887101..36a022fd98 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -50,7 +50,7 @@ open Pre_env (* Access to these variables is performed by the [Koffsetclosure n] *) (* instruction that shifts the environment pointer of [n] fields. *) -(* This allows to represent mutual fixpoints in just one block. *) +(* This allows representing mutual fixpoints in just one block. *) (* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint *) (* types. They are used in conversion tests (which requires that *) (* fixpoint types must be convertible). Their environment is the one of *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ff5ce284e7..18ebc2aa03 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -220,7 +220,7 @@ let typecheck_inductive env ctx mie = let env' = push_context ctx env in let (env_params, params) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) - (* This allows to build the environment of arities and to share *) + (* This allows building the environment of arities and to share *) (* the set of constraints *) let env_arities, rev_arity_list = List.fold_left @@ -633,7 +633,7 @@ let allowed_sorts is_smashed s = (* Previous comment: *) (* Unitary/empty Prop: elimination to all sorts are realizable *) (* unless the type is large. If it is large, forbids large elimination *) -(* which otherwise allows to simulate the inconsistent system Type:Type. *) +(* which otherwise allows simulating the inconsistent system Type:Type. *) (* -> this is now handled by is_smashed: *) (* - all_sorts in case of small, unitary Prop (not smashed) *) (* - logical_sorts in case of large, unitary Prop (smashed) *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9140d171d0..bac242f823 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -99,7 +99,7 @@ val check_cofix : env -> cofixpoint -> unit (** {6 Support for sort-polymorphic inductive types } *) -(** The "polyprop" optional argument below allows to control +(** The "polyprop" optional argument below controls the "Prop-polymorphism". By default, it is allowed. But when "polyprop=false", the following exception is raised when a polymorphic singleton inductive type becomes Prop due to diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 466380f2d6..5a2f5ced78 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -19,7 +19,7 @@ open Term (* Type declarations, these types shouldn't be exported they are accessed through specific functions. As being mutable and all it is wiser *) (* These types are put into two distinct categories: proactive and reactive. - Proactive information allows to find the name of a combinator, constructor + Proactive information allows finding the name of a combinator, constructor or inductive type handling a specific function. Reactive information is, on the other hand, everything you need to know about a specific name.*) |