diff options
| -rw-r--r-- | test-suite/success/Notations.v | 6 | ||||
| -rw-r--r-- | toplevel/command.ml | 3 |
2 files changed, 8 insertions, 1 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 511b60b4bb..8c83b196e4 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -116,3 +116,9 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). Goal True. {{ exact I. }} Qed. + +(* Check "where" clause for inductive types with parameters *) + +Reserved Notation "x === y" (at level 50). +Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x + where "x === y" := (EQ x y). diff --git a/toplevel/command.ml b/toplevel/command.ml index b9e4dbd7b2..8926b410c6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -571,12 +571,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = lift_implicits (rel_context_nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in + let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in |