diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-26 18:51:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-26 18:51:53 +0000 |
| commit | b6c570ac655085c0af402e3e4546c4904fa015d0 (patch) | |
| tree | 65007bda78e83fa083a1afed2a0196cc00bc38c3 /library/global.ml | |
| parent | a58feae47d627b482c2e0fbdf5ec93fecf4b5435 (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/global.ml')
| -rw-r--r-- | library/global.ml | 6 |
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 |