diff options
Diffstat (limited to 'parsing/vernacextend.ml4')
| -rw-r--r-- | parsing/vernacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 58946eda9..cc3bd07e8 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -36,7 +36,7 @@ let check_unicity s l = let make_clause (_,pt,e) = (make_patt pt, - Some (make_when (MLast.loc_of_expr e) pt), + vala (Some (make_when (MLast.loc_of_expr e) pt)), make_let e pt) let make_fun_clauses loc s l = |