diff options
Diffstat (limited to 'tuto1/src/g_tuto1.ml4')
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 index e171688083..1f4660d1f0 100644 --- a/tuto1/src/g_tuto1.ml4 +++ b/tuto1/src/g_tuto1.ml4 @@ -81,7 +81,7 @@ VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF | [ "Cmd4" ident(i) constr(e) ] -> [ let v = Constrintern.interp_constr (Global.env()) (Evd.from_env (Global.env())) e in - Simple_declare.packed_declare_definition i v ] + Simple_declare.packed_declare_definition ~poly:(Attributes.(parse polymorphic atts)) i v ] END VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY |