aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bc8debd02..6704ed4b7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -967,7 +967,7 @@ and extern_local_binder scopes vars = function
(assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
- Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
+ Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl],
extern inctx scopes vars c)
and extern_notation (tmp_scope,scopes as allscopes) vars t = function