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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/hints.ml | 10 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 3 |
4 files changed, 9 insertions, 10 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index d0f4b2c680..510f119229 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -356,9 +356,9 @@ let find_elim hdcncl lft2rgt dep cls ot = | Some true, None | Some false, Some _ -> let c1 = destConstRef pr1 in - let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in + let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in + let c1' = Global.constant_of_delta_kn (KerName.make mp l') in begin try let _ = Global.lookup_constant c1' in diff --git a/tactics/hints.ml b/tactics/hints.ml index c0ba363360..90eafe88c4 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -209,14 +209,14 @@ let fresh_key = let cur = incr id; !id in let lbl = Id.of_string ("_" ^ string_of_int cur) in let kn = Lib.make_kn lbl in - let (mp, dir, _) = KerName.repr kn in + let (mp, _) = KerName.repr kn in (** We embed the full path of the kernel name in the label so that the identifier should be unique. This ensures that including two modules together won't confuse the corresponding labels. *) - let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" - (ModPath.to_string mp) (DirPath.to_string dir) cur) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%i" + (ModPath.to_string mp) cur) in - KerName.make mp dir (Label.of_id lbl) + KerName.make mp (Label.of_id lbl) let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) = let d = pri1 - pri2 in @@ -1601,7 +1601,7 @@ let warn_non_imported_hint = let warn env sigma h = let hint = pr_hint env sigma h in - let (mp, _, _) = KerName.repr h.uid in + let mp = KerName.modpath h.uid in warn_non_imported_hint (hint,mp) let wrap_hint_warning t = diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 7da059ae35..a1bb0a7401 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -438,7 +438,7 @@ let match_eq sigma eqn (ref, hetero) = | _ -> raise PatternMatchingFailure let no_check () = true -let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module +let check_jmeq_loaded () = Library.library_is_loaded @@ Coqlib.jmeq_library_path let equalities = [(coq_eq_ref, false), no_check, build_coq_eq_data; diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e4013152e6..b81967c781 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -56,8 +56,7 @@ let subst_scheme (subst,(kind,l)) = (kind,Array.Smart.map (subst_one_scheme subst) l) let discharge_scheme (_,(kind,l)) = - Some (kind,Array.map (fun (ind,const) -> - (Lib.discharge_inductive ind,Lib.discharge_con const)) l) + Some (kind, l) let inScheme : string * (inductive * Constant.t) array -> obj = declare_object {(default_object "SCHEME") with |