diff options
| author | Maxime Dénès | 2018-09-25 14:33:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-05 08:57:56 +0200 |
| commit | 650c65af484c45f4e480252b55d148bcc198be6c (patch) | |
| tree | ebc0a8e7777ddd90515abcdea2e8975d1d968640 /plugins/syntax/r_syntax.ml | |
| parent | 3f2a6d8e99f31bbd9383119cac39ed0bcaabc37d (diff) | |
[kernel] Remove section paths from `KerName.t`
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
Diffstat (limited to 'plugins/syntax/r_syntax.ml')
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 49497aef54..776d2a2229 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -33,12 +33,10 @@ let is_gr c gr = match DAst.get c with | GRef (r, _) -> GlobRef.equal r gr | _ -> false +let positive_modpath = MPfile (make_dir binnums) let positive_path = make_path binnums "positive" -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") +let positive_kn = MutInd.make2 positive_modpath (Label.make "positive") let glob_positive = IndRef (positive_kn,0) let path_of_xI = ((positive_kn,0),1) let path_of_xO = ((positive_kn,0),2) @@ -74,7 +72,7 @@ let rec bignat_of_pos c = match DAst.get c with (**********************************************************************) let z_path = make_path binnums "Z" -let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") +let z_kn = MutInd.make2 positive_modpath (Label.make "Z") let glob_z = IndRef (z_kn,0) let path_of_ZERO = ((z_kn,0),1) let path_of_POS = ((z_kn,0),2) @@ -106,12 +104,10 @@ let bigint_of_z c = match DAst.get c with (**********************************************************************) let rdefinitions = ["Coq";"Reals";"Rdefinitions"] +let r_modpath = MPfile (make_dir rdefinitions) let r_path = make_path rdefinitions "R" -(* TODO: temporary hack *) -let make_path dir id = Globnames.encode_con dir (Id.of_string id) - -let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") +let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") let r_of_int ?loc z = DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) |