diff options
| -rw-r--r-- | interp/constrintern.ml | 20 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5762.v | 6 | ||||
| -rw-r--r-- | test-suite/success/Notations2.v | 6 |
3 files changed, 24 insertions, 8 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a0a749bfb3..e20a159f89 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -534,8 +534,9 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function | Name id -> try (* Binders bound in the notation are considered first-order objects *) - let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na + let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in + let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in + (renaming,env), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -747,7 +748,14 @@ let gvar (loc, id) us = match us with str " cannot have a universe instance") let intern_var genv (ltacvars,ntnvars) namedctx loc id us = - (* Is [id] an inductive type potentially with implicit *) + (* Is [id] a notation variable *) + if Id.Map.mem id ntnvars then + begin + if not (Id.Map.mem id genv.impls) then set_var_scope ?loc id true genv ntnvars; + gvar (loc,id) us, [], [], [] + end + else + (* Is [id] registered with implicit arguments *) try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in let expl_impls = List.map @@ -760,12 +768,8 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars then gvar (loc,id) us, [], [], [] - (* Is [id] a notation variable *) - else if Id.Map.mem id ntnvars - then - (set_var_scope ?loc id true genv ntnvars; gvar (loc,id) us, [], [], []) - (* Is [id] the special variable for recursive notations *) else if Id.equal id ldots_var + (* Is [id] the special variable for recursive notations? *) then if Id.Map.is_empty ntnvars then error_ldots_var ?loc else gvar (loc,id) us, [], [], [] diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v index edd5c8d73d..55d36bd722 100644 --- a/test-suite/bugs/closed/5762.v +++ b/test-suite/bugs/closed/5762.v @@ -26,3 +26,9 @@ Reserved Notation "%% a" (at level 70). Record R := {g : forall {A} (a:A), a=a where "%% x" := (g x); k : %% 0 = eq_refl}. + +(* An extra example *) + +Module A. +Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I) : I_scope. +End A. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 9505a56e3f..e86b3edb83 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -90,3 +90,9 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. Notation "##### x" := (pair' x) (at level 0, x at level 1). Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. + +(* 10. Check computation of binding variable through other notations *) +(* i should be detected as binding variable and the scopes not being checked *) + +Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). +Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). |