diff options
Diffstat (limited to 'parsing/tacextend.ml4')
-rw-r--r-- | parsing/tacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index e1ae91966..ec305ee2e 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -59,7 +59,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 = |