aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/closure.mli')
-rw-r--r--kernel/closure.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli
index ede0d6379..b6ff1fa15 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -24,7 +24,7 @@ val with_stats: 'a Lazy.t -> 'a
(*s Delta implies all consts (both global (= by
[kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
- Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
+ Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
@@ -102,7 +102,7 @@ type fconstr
type fterm =
| FRel of int
| FAtom of constr (* Metas and Sorts *)
- | FCast of fconstr * cast_kind * fconstr
+ | FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of inductive
| FConstruct of constructor