diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.mli | 2 | ||||
| -rw-r--r-- | vernac/comHints.ml | 1 | ||||
| -rw-r--r-- | vernac/declare.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
5 files changed, 7 insertions, 4 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index e1816fb138..89ff4e6939 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -81,7 +81,7 @@ val add_class : env -> Evd.evar_map -> typeclass -> unit (** Setting opacity *) -val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit +val set_typeclass_transparency : Tacred.evaluable_global_reference -> bool -> bool -> unit (** For generation on names based on classes only *) diff --git a/vernac/comHints.ml b/vernac/comHints.ml index f642411fa4..1c36e10e83 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -76,6 +76,7 @@ let warn_deprecated_hint_constr = *) let soft_evaluable = let open GlobRef in + let open Tacred in function | ConstRef c -> EvalConstRef c | VarRef id -> EvalVarRef id diff --git a/vernac/declare.ml b/vernac/declare.ml index fafee13bf6..c715304419 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -883,7 +883,7 @@ let shrink_body c ty = (* Saving an obligation *) (***********************************************************************) -let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] +let unfold_entry cst = Hints.HintsUnfoldEntry [Tacred.EvalConstRef cst] let add_hint local prg cst = let locality = if local then Goptions.OptLocal else Goptions.OptExport in diff --git a/vernac/record.ml b/vernac/record.ml index 583164a524..68219603b4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -625,7 +625,7 @@ let build_class_constant ~univs ~rdata field implfs params paramimpls coers bind let cref = GlobRef.ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs); - Classes.set_typeclass_transparency (EvalConstRef cst) false false; + Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false; let sub = List.hd coers in let m = { meth_name = Name proj_name; @@ -744,7 +744,7 @@ let add_constant_class env sigma cst = } in Classes.add_class env sigma tc; - Classes.set_typeclass_transparency (EvalConstRef cst) false false + Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false let add_inductive_class env sigma ind = let mind, oneind = Inductive.lookup_mind_specif env ind in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a3726daf63..e8cb1d65a9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1628,6 +1628,7 @@ let () = } let vernac_set_strategy ~local l = + let open Tacred in let local = Option.default false local in let glob_ref r = match smart_global r with @@ -1639,6 +1640,7 @@ let vernac_set_strategy ~local l = Redexpr.set_strategy local l let vernac_set_opacity ~local (v,l) = + let open Tacred in let local = Option.default true local in let glob_ref r = match smart_global r with |