| Age | Commit message (Expand) | Author |
|---|
| 2011-07-26 | Integral domains | pottier |
| 2011-07-26 | Ring2 devient Ncring et la reification par les type classes est partagee | pottier |
| 2011-07-22 | Add a syntax entry for fully applied constructor pattern | pboutill |
| 2011-07-04 | Set Extraction KeepSingleton: an option for not decapsulating singleton types | letouzey |
| 2011-07-04 | Extraction: in haskell, __ may have any type, no need to unsafeCoerce it | letouzey |
| 2011-07-04 | Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552) | letouzey |
| 2011-07-04 | Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml | letouzey |
| 2011-06-30 | Fix compilation error | msozeau |
| 2011-06-30 | Keep obligation source information in Program | msozeau |
| 2011-06-29 | update of Micromega doc | fbesson |
| 2011-06-28 | Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def | letouzey |
| 2011-06-28 | improved tactic names | fbesson |
| 2011-06-24 | Numbers: a particular case of div_unique | letouzey |
| 2011-06-21 | Follow-up concerning eqb / ltb / leb comparisons | letouzey |
| 2011-06-21 | Cleaning debugging printer relative to new proof engine. In | herbelin |
| 2011-06-18 | Relaxed the constraint introduced in r14190 that froze the existing | herbelin |
| 2011-06-17 | Fix bug 2269, program typechecker not used in Instance conclusions | msozeau |
| 2011-06-16 | Tests de nsatz avec la geometrie | pottier |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-06-10 | Call process_vernac_interp_error before calling Errors.print in | herbelin |
| 2011-06-10 | Revert "Check if recursive calls are guarded before printing "Proof completed"." | pboutill |
| 2011-06-10 | ring2, cring, nsatz avec type classe avec parametres plus notations | pottier |
| 2011-06-07 | Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn... | msozeau |
| 2011-06-07 | Fix bug #2415: warn when closing modules or sections and some obligations are... | msozeau |
| 2011-05-26 | Check if recursive calls are guarded before printing "Proof completed". | herbelin |
| 2011-05-25 | Q2R -> IQR | fbesson |
| 2011-05-24 | Made the emacs-U option deprecated. Also removed the old code | courtieu |
| 2011-05-23 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0... | fbesson |
| 2011-05-20 | added support to handle division by a constant over R | fbesson |
| 2011-05-19 | Extraction: avoid lots of late mind_of_kn | letouzey |
| 2011-05-19 | Extraction: global reference should be indexed on their user part (fix #2540) | letouzey |
| 2011-05-18 | cbv delta - [...] before calling lia | fbesson |
| 2011-05-18 | apply zeta reduction before syntaxification | fbesson |
| 2011-05-18 | Extraction: avoid printing of Recursive Extraction in coqide's console | letouzey |
| 2011-05-16 | Fixed my last patch: these files no longer use nat_beq (automatically | vsiles |
| 2011-05-13 | A new mechanism to handle errors. | aspiwack |
| 2011-05-11 | Print Module (Type) M now tries to print more details | letouzey |
| 2011-05-09 | Improved lia + experimental nlia | fbesson |
| 2011-05-06 | Additionnal fix of romega after modularisation of ZArith | letouzey |
| 2011-05-05 | Modularisation of Znat, a few name changed elsewhere | letouzey |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | letouzey |
| 2011-05-05 | Modularization of BinInt, related fixes in the stdlib | letouzey |
| 2011-05-05 | Setoid_ring: some cleanups related with BinPos and BinNat | letouzey |
| 2011-05-05 | Modularization of BinNat + fixes of stdlib | letouzey |
| 2011-05-05 | Modularization of Pnat | letouzey |
| 2011-05-05 | Modularization of BinPos + fixes in Stdlib | letouzey |
| 2011-05-05 | Definitions of positive, N, Z moved in Numbers/BinNums.v | letouzey |
| 2011-05-05 | Extraction: allow extraction foo when foo is an alias notation | letouzey |
| 2011-05-04 | First phase removing obsolete support for eta up to conversion in | herbelin |
| 2011-04-29 | Fixed a bug causing inconsistent states during proof editting. | aspiwack |
