diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ca3c77aad..9809d4d09 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -89,10 +89,12 @@ type tomatch_type = (* spiwack: The first argument of [Pushed] is [true] for initial Pushed and [false] otherwise. Used to decide whether the term being matched on must be aliased in the variable case (only initial - Pushed need to be aliased). *) + Pushed need to be aliased). The first argument of [Alias] is [true] + if the alias was introduced by an initial pushed and [false] + otherwise.*) type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) - | Alias of (Name.t * constr * (constr * types)) + | Alias of (bool * (Name.t * constr * (constr * types))) | NonDepAlias | Abstract of int * rel_declaration |