aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8d3cf7274a..aa3a458989 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1303,7 +1303,8 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
termlists in
let bl =
List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
- mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
+ (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)),
+ Explicit)
binders in
let bll =
List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->