diff options
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index fa302de64..260d159b3 100644 --- a/checker/closure.mli +++ b/checker/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 *) type transparent_state = Idpred.t * Cpred.t @@ -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 |