| Age | Commit message (Collapse) | Author |
|---|
|
Instead, we register functions dynamically declaring the dependencies of the
scheme to be generated.
We had to fix the test-suite because an internal scheme name changed.
We could also tweak the internal flag of scheme dependencies, but in this
particular case it looks more like a bug from the previous implementation.
|
|
so for instance
~~~coq
Set Printing All. Set Printing Universes.
Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
Lemma bla@{u v|u < v} : foo@{u v} -> False.
Proof. induction 1. Qed.
~~~
works.
|
|
- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14195 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14193 85f007b7-540e-0410-9357-904b9bb8a0f7
|
