diff options
| author | Guillaume Melquiond | 2015-12-07 10:52:14 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-12-07 10:52:24 +0100 |
| commit | df3a49a18c5b01984000df9244ecea9c275b30cd (patch) | |
| tree | d14afdb5de5f93e4301f8eba8bddecd5a6597f9a /kernel/closure.ml | |
| parent | fe2776f9e0d355cccb0841495a9843351d340066 (diff) | |
Fix some typos.
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index ea9b2755f2..03e70495fb 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -771,7 +771,7 @@ let drop_parameters depth n argstk = (* we know that n < stack_args_size(argstk) (if well-typed term) *) anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. |