diff options
| author | herbelin | 2012-03-20 08:02:20 +0000 |
|---|---|---|
| committer | herbelin | 2012-03-20 08:02:20 +0000 |
| commit | 2e23b8850d533f94d7bab6d58afb7044c5cb4f66 (patch) | |
| tree | 1ea2cde82d1ecb5eb91d1f3d5fdc8e4196ee3c37 /plugins/xml | |
| parent | 75d51735e95d43323b03ecf586c6aba163cf70a6 (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/xml')
0 files changed, 0 insertions, 0 deletions