aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/declarations.ml
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 /checker/declarations.ml
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 'checker/declarations.ml')
0 files changed, 0 insertions, 0 deletions