aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorherbelin2012-03-20 08:02:20 +0000
committerherbelin2012-03-20 08:02:20 +0000
commit2e23b8850d533f94d7bab6d58afb7044c5cb4f66 (patch)
tree1ea2cde82d1ecb5eb91d1f3d5fdc8e4196ee3c37 /plugins
parent75d51735e95d43323b03ecf586c6aba163cf70a6 (diff)
Use a careful analysis of dependencies in restricting instances to
solve the following kind of code broken by being less restrictive on projecting: Set Printing Existential Instances. Parameter f : forall x, x=0 -> x=0 -> x=1 /\ x=2. Parameter g : forall y, y=0 /\ y=0. Check match g _ with conj a b => f _ a b end. (* and the return clause should not depend on the "_" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15064 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions