diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 14:44:28 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | a9d151a31937724543d5269e72b0262c8764c46e (patch) | |
| tree | c88761514ebb3b4ff2691acf8dcfec6f13135d97 /interp/constrexpr_ops.ml | |
| parent | 158f40db9482ead89befbf9bc9ad45ff8a60b75f (diff) | |
[location] More located use.
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 4f23dd2ab..61115c00b 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -239,7 +239,7 @@ let local_binder_loc = function | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t) | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t)) | CLocalAssum ([],_,_) -> assert false - | CLocalPattern (loc,_,_) -> loc + | CLocalPattern (loc,_) -> loc let local_binders_loc bll = match bll with | [] -> Loc.ghost @@ -283,7 +283,7 @@ let expand_binders ~loc mkC bl c = let env = List.fold_left add_name_in_env env nl in (env, mkC ~loc (nl,bk,t) c) | CLocalAssum ([],_,_) -> loop loc bl c - | CLocalPattern (loc1, p, ty) -> + | CLocalPattern (loc1, (p, ty)) -> let env, c = loop ~loc:(Loc.merge loc1 loc) bl c in let ni = Hook.get fresh_var env c in let id = (loc1, Name ni) in |