From 4af1609cd70cca670109dfd6dfa06ed02034f7ae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 18 Jul 2017 13:34:14 +0200
Subject: Fixing a little location bug with recursive binders.

Note that localisation cannot be perfect anyways, as in the following
example, where there is no way to highlight in the original input a
syntactically stand-alone subterm where the error occurs.

> Check forall (y:nat) (x:=0), y.
>       ^^^^^^^^^^^^^^^^^^^^^^^^
Error: In environment
y : nat
The term "let x := 0 in y" has type "nat" which should be Set, Prop or Type.
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f360fb192f..c9fc3aa4f3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -664,11 +664,11 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
     | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
         let e = make_letins letins (aux subst' infos c') in
-        let (loc,(na,bk,t)) = a in
+        let (_loc,(na,bk,t)) = a in
         CAst.make ?loc @@ GProd (na,bk,t,e)
     | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
-        let (loc,(na,bk,t)) = a in
+        let (_loc,(na,bk,t)) = a in
         CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
-- 
cgit v1.2.3