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, 1 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 362fe83ffa..7f5f03610b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,8 +1211,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
let (t,args,argsscopes,argsimpls) = match n with
| Some n when nallargs >= n ->
let args1, args2 = List.chop n args in
- let args2scopes =
- if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+ let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
let args2impls =
if n = 0 then
(* Note: NApp(NRef f,[]), hence n=0, encodes @f and