lp:coq
- Get this branch:
- bzr branch lp:coq
Branch merges
Branch information
Recent revisions
- 10699. By herbelin
-
Experiment propagation of implicit arguments and arguments scope for
abbreviations of applied references. - 10697. By letouzey
-
Repair interpretation of numeral for BigQ, add a printer (close #2160)
on the way:
- Added a testsuite output file
- Try to avoid nasty unfolding (fix nfun ...) in type of I31.
Idealy we would need a "Eval compute in" for the type of a inductive
constructor
- Stop opening Scopes for BigQ, BigN, BigZ by default
The user should do some Open Scope.TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope
(and so on for other operations), even with some Bind Scope around. - 10696. By letouzey
-
Better compatibility for Peqb
As show by contrib TreeAutomata, the Peqb now placed in BinPos
was using 1st arg as "struct", instead of 2nd arg as earlier.
Fix that, and remove the "Import BinPos BinNat" hack in Ndec
(merci Hugo :-). - 10694. By herbelin
-
Backtracking on the use of automatically generated schemes for
"eq"-rewriting (a few contributions are still referring explicitly to
eq_rect, eq_ind and co and the new mechanism, though working also for
dependent rewriting, is not powerful enough in general wrt fixpoint
guard to claim being uniformly better). - 10692. By herbelin
-
Redoing broken commit r12498 (fixing bug #2167 + attempt to test the
compatibility of a more robust check of unconvertibility when
providing "with" arguments to "apply").
Branch metadata
- Branch format:
- Branch format 7
- Repository format:
- Bazaar repository format 2a (needs bzr 1.16 or later)