diff options
| author | Hugo Herbelin | 2017-07-18 13:34:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-07-18 13:38:42 +0200 |
| commit | 4af1609cd70cca670109dfd6dfa06ed02034f7ae (patch) | |
| tree | 4a81a8c034288099b7e2e5f41c8efbb7874156f3 /interp | |
| parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
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.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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') |