aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-17 14:44:28 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-24 23:58:23 +0200
commita9d151a31937724543d5269e72b0262c8764c46e (patch)
treec88761514ebb3b4ff2691acf8dcfec6f13135d97 /interp/constrextern.ml
parent158f40db9482ead89befbf9bc9ad45ff8a60b75f (diff)
[location] More located use.
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 bbc98dd28..8d9f8552d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -866,7 +866,7 @@ and extern_local_binder scopes vars = function
if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
let p = extern_cases_pattern vars p in
let (assums,ids,l) = extern_local_binder scopes vars l in
- (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l)
+ (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],