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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 18 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 |
2 files changed, 10 insertions, 10 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 148d4437fa..9f71def8fc 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -63,20 +63,20 @@ exception ConstructorWithNonParametricInductiveType of inductive exception DecidabilityIndicesNotSupported (* Some pre declaration of constant we are going to use *) -let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop") +let andb_prop = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_prop") let andb_true_intro = fun _ -> - UnivGen.constr_of_global + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_true_intro") (* We avoid to use lazy as the binding of constants can change *) -let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type") -let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true") -let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false") -let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type") +let bb () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.type") +let tt () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.true") +let ff () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.false") +let eq () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type") -let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type") -let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb") +let sumbool () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.sumbool.type") +let andb = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb") let induct_on c = induction false None c None None let destruct_on c = destruct false None c None None @@ -873,7 +873,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) ) ) ) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 0ac97a74e4..fbf552e649 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -266,7 +266,7 @@ let eterm_obligations env name evm fs ?status t ty = let hide_obligation () = Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation") + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation") let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) |