lp:coq

Branch merges

Propose for merging

No branches dependent on this one.

Related source package recipes

No recipes using this branch. (?)

Related snap packages

Related bugs

Related blueprints

10699. By herbelin on 2009-11-12

Experiment propagation of implicit arguments and arguments scope for
abbreviations of applied references.

10698. By herbelin on 2009-11-12

Addendum to revision 12501.

10697. By letouzey on 2009-11-12

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 on 2009-11-11

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 :-).

10695. By glondu on 2009-11-11

Promote evar_defs to evar_map (in Evd)

10694. By herbelin on 2009-11-11

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).

10693. By herbelin on 2009-11-11

Added support for multiple where-clauses in Inductive and co (see wish #2163).

10692. By herbelin on 2009-11-11

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").

10691. By herbelin on 2009-11-11

Fixing bug #2167 + attempt to test the compatibility of a more robust
check of unconvertibility when providing "with" arguments to "apply".

10690. By herbelin on 2009-11-11

Test for bug #2168, forgotten in r12496.