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/funind/indfun.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/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9eda19a86b..9a6169d42a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -898,11 +898,11 @@ let make_graph (f_ref : GlobRef.t) = let id = Label.to_id (Constant.label c) in [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in - let mp,dp,_ = Constant.repr3 c in + let mp = Constant.modpath c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; (* We register the infos *) List.iter - (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) + (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) expr_list) let do_generate_principle = do_generate_principle [] warning_error true |