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 /toplevel | |
| 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).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |