diff options
| author | Hugo Herbelin | 2020-10-24 13:18:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-20 19:41:20 +0100 |
| commit | 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa (patch) | |
| tree | 9f2812eedcabf7dcfb8f6edc824ae51a06c27c87 /interp/constrexpr.ml | |
| parent | 52b93b587b9cb53b0ed11c7d6cf5f328d7ee1479 (diff) | |
A step towards supporting pattern cast deeplier.
We at least support a cast at the top of patterns in notations.
Diffstat (limited to 'interp/constrexpr.ml')
| -rw-r--r-- | interp/constrexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index a5ff5df7cf..b3f06faa1c 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -147,7 +147,7 @@ and recursion_order_expr = recursion_order_expr_r CAst.t and local_binder_expr = | CLocalAssum of lname list * binder_kind * constr_expr | CLocalDef of lname * constr_expr * constr_expr option - | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t + | CLocalPattern of cases_pattern_expr and constr_notation_substitution = constr_expr list * (* for constr subterms *) |