diff options
| author | Matthieu Sozeau | 2018-10-12 18:15:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-18 14:18:24 +0200 |
| commit | e050884da17b260934a428d5b1bb11cd788ae0e1 (patch) | |
| tree | 579f4b8f99b7832d75ff2ead82ae209b41033ec0 /engine | |
| parent | 88ecdf6b51b0d7b4cde335cf94297c102d7d551e (diff) | |
[universes] deprecate constr_of_global
In favor of a constr_of_monomorphic_global function. When people
move to the new Coqlib interface they will also see this deprecation
message encouraging them to think about the best move.
This commit changes a few references to constr_of_global and replaces
them with a constr_of_monomorphic_global which makes it apparent that
this is not the function to call to globalize polymorphic references.
The remaining parts using constr_of_monomorphic_global are easily
identifiable using this: omega, btauto, ring, funind and auto_ind_decl
mainly (this fixes firstorder). What this means is that the symbols
registered for these tactics have to be monomorphic for now.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univGen.ml | 19 | ||||
| -rw-r--r-- | engine/univGen.mli | 9 |
2 files changed, 15 insertions, 13 deletions
diff --git a/engine/univGen.ml b/engine/univGen.ml index 23ab30eb75..130aa06f53 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -77,17 +77,14 @@ let fresh_global_instance ?loc ?names env gr = let u, ctx = fresh_global_instance ?loc ?names env gr in mkRef (gr, u), ctx -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else CErrors.user_err ~hdr:"constr_of_global" - Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ - str " would forget universes.") - else c +let constr_of_monomorphic_global gr = + if not (Global.is_polymorphic gr) then + fst (fresh_global_instance (Global.env ()) gr) + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + +let constr_of_global gr = constr_of_monomorphic_global gr let constr_of_global_univ = mkRef diff --git a/engine/univGen.mli b/engine/univGen.mli index c2e9d0c696..42756701dc 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -74,11 +74,16 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> [@@ocaml.deprecated "Use [Univ.extend_in_context_set]"] (** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) + the proper way to get a fresh copy of a polymorphic global reference. *) +val constr_of_monomorphic_global : GlobRef.t -> constr + val constr_of_global : GlobRef.t -> constr +[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\ + use [constr_of_monomorphic_global] if the reference is guaranteed to\ + be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"] (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the |