diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 21:26:48 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-17 10:56:07 +0100 |
| commit | 1172b52735a299dfc91aee36b30b576dfeff581c (patch) | |
| tree | 67c42534af08f70d0eeefe78245483867cdb1248 /vernac/classes.ml | |
| parent | 7a5688f6e2421a706c16e23e445d42f39a82e74b (diff) | |
[flags] Make program_mode a parameter for commands in vernac.
This is useful as it allows to reflect program_mode behavior as an attribute.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 3d9c7defa..c2e9a5ab4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -130,7 +130,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t id let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) - poly ctx (instid, bk, cl) props ?(generalize=true) + ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ((loc, instid), pl) = instid in @@ -215,7 +215,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Some (Inl fs) | Some (_, t) -> Some (Inr t) | None -> - if Flags.is_program_mode () then Some (Inl []) + if program_mode then Some (Inl []) else None in let subst, sigma = @@ -297,9 +297,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype - else if Flags.is_program_mode () || refine || Option.is_empty term then begin + else if program_mode || refine || Option.is_empty term then begin let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in - if Flags.is_program_mode () then + if program_mode then let hook vis gr _ = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; |