aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-26 18:51:53 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-26 18:51:53 +0000
commitb6c570ac655085c0af402e3e4546c4904fa015d0 (patch)
tree65007bda78e83fa083a1afed2a0196cc00bc38c3 /library
parenta58feae47d627b482c2e0fbdf5ec93fecf4b5435 (diff)
Mod_subst: misc reformulations
* Remove the mind_of_delta and constant_of_delta functions, prefer instead the {mind,constant}_of_delta_kn functions. * Attempt to make subst_ind and subst_con0 more self-contained git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/global.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/library/global.ml b/library/global.ml
index e47085c89..3b911e229 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -122,14 +122,12 @@ let constant_of_delta_kn kn =
(* TODO : are resolver and resolver_param orthogonal ?
the effect of resolver is lost if resolver_param isn't
trivial at that spot. *)
- Mod_subst.constant_of_delta resolver_param
- (Mod_subst.constant_of_delta_kn resolver kn)
+ Mod_subst.constant_of_deltas_kn resolver_param resolver kn
let mind_of_delta_kn kn =
let resolver,resolver_param = (delta_of_senv !global_env) in
(* TODO idem *)
- Mod_subst.mind_of_delta resolver_param
- (Mod_subst.mind_of_delta_kn resolver kn)
+ Mod_subst.mind_of_deltas_kn resolver_param resolver kn
let exists_objlabel id = exists_objlabel id !global_env