diff options
| author | Gaëtan Gilbert | 2018-10-16 16:45:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:28:58 +0100 |
| commit | e6c64a54f8f52ff555a0857a2909f5f70b22e591 (patch) | |
| tree | 8d986606f5ed977bcd57397de930d6f88ee322ee | |
| parent | 58b9174b229863c694ad65984b86b112c689ae10 (diff) | |
Fix for coq/coq#8515 (command driven attributes)
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 2 | ||||
| -rw-r--r-- | tuto1/src/simple_declare.ml | 5 | ||||
| -rw-r--r-- | tuto1/src/simple_declare.mli | 2 |
3 files changed, 4 insertions, 5 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 diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index 2737793d69..af4dd5bddf 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -13,11 +13,10 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = let ce = Declare.definition_entry ?types:tyopt ~univs body in DeclareDef.declare_definition ident k ce ubinders imps hook -let packed_declare_definition ident value_with_constraints = +let packed_declare_definition ~poly ident value_with_constraints = let body, ctx = value_with_constraints in let sigma = Evd.from_ctx ctx in - let k = (Decl_kinds.Global, - Flags.is_universe_polymorphism(), Decl_kinds.Definition) in + let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in let udecl = UState.default_univ_decl in let nohook = Lemmas.mk_hook (fun _ x -> ()) in ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) diff --git a/tuto1/src/simple_declare.mli b/tuto1/src/simple_declare.mli index 7a28626d88..fd74e81526 100644 --- a/tuto1/src/simple_declare.mli +++ b/tuto1/src/simple_declare.mli @@ -2,4 +2,4 @@ open Names open EConstr val packed_declare_definition : - Id.t -> constr Evd.in_evar_universe_context -> unit
\ No newline at end of file + poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit |