aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-02 22:08:30 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-02 22:08:30 +0000
commit5635c35ea4ec172fd81147effed4f33e2f581aaa (patch)
tree303bb7d5a991cef2edbd4899e50a10b47d39e1b5 /library/states.ml
parent42cbb18f5b0e220a832ccf5db320d90be5ce0c8e (diff)
Mod_subst.force: avoid using join when only one subst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/states.ml')
0 files changed, 0 insertions, 0 deletions