aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/tacextend.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/tacextend.ml4')
-rw-r--r--parsing/tacextend.ml42
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 =