diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 9019fa091..cd86af675 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -100,7 +100,7 @@ type 'ctxt reference = (* Concrete type for making pattern-matching. *) -(* [constr array] is an instance matching definitional var_context in +(* [constr array] is an instance matching definitional [var_context] in the same order (i.e. last argument first) *) type existential = int * constr array type constant = section_path * constr array |