aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cClosure.ml
diff options
context:
space:
mode:
authorGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-03 11:06:48 +0000
committerGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-05 14:35:30 +0000
commit1f0d1f04b704e3368a12613f31061a53a2e40d01 (patch)
tree2dd28a7d2bfa1e5a5fc8e50f293b8371db67edc8 /kernel/cClosure.ml
parentc84509113e08372e9aa30eae57ce98f56ca95bde (diff)
Replace invalid tag @raises in ocamldoc comments with @raise
Diffstat (limited to 'kernel/cClosure.ml')
-rw-r--r--kernel/cClosure.ml2
1 files changed, 1 insertions, 1 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') =