diff options
| author | Hugo Herbelin | 2017-02-23 14:34:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-02-23 14:52:35 +0100 |
| commit | fedc831df9626a31cd0d26ee6b9e022b67f90c2a (patch) | |
| tree | a2b66571ca95f3460b6818f2f0716e68bfeee133 | |
| parent | 4ddf3ee41eb6e8faaf223041d2bd42d4c62be58d (diff) | |
Fixing a little bug in using the "where" clause for inductive types.
This was not working when the inductive type had implicit parameters.
This could still be improved. E.g. the following still does not work:
Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.
But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).
| -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 |