diff options
| author |  mrmr1993 <mr_1993@hotmail.co.uk> | 2018-03-03 11:06:48 +0000 |
|---|---|---|
| committer | mrmr1993 <mr_1993@hotmail.co.uk> | 2018-03-05 14:35:30 +0000 |
| commit | 1f0d1f04b704e3368a12613f31061a53a2e40d01 (patch) | |
| tree | 2dd28a7d2bfa1e5a5fc8e50f293b8371db67edc8 /kernel | |
| parent | c84509113e08372e9aa30eae57ce98f56ca95bde (diff) | |
Replace invalid tag @raises in ocamldoc comments with @raise
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 2 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 2 | ||||
| -rw-r--r-- | kernel/environ.mli | 2 | ||||
| -rw-r--r-- | kernel/uGraph.mli | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c5a8c7b23..11faef02c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -798,7 +798,7 @@ let drop_parameters depth n argstk = s. @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 71453a04b..b9c71d72a 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -216,7 +216,7 @@ val whd_stack : s. @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> diff --git a/kernel/environ.mli b/kernel/environ.mli index 51388b8f3..ce2bf85c3 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -201,7 +201,7 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) (** Add universe constraints to the environment. - @raises UniverseInconsistency + @raise UniverseInconsistency *) val add_constraints : Univ.Constraint.t -> env -> env diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 97745771e..d4fba63fb 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -43,7 +43,7 @@ val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared |