| Commit message (Expand) | Author | Age |
* | 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-07-04 |
* | Fix compilation error | msozeau | 2011-06-30 |
* | Keep obligation source information in Program | msozeau | 2011-06-30 |
* | update of Micromega doc | fbesson | 2011-06-29 |
* | Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def | letouzey | 2011-06-28 |
* | improved tactic names | fbesson | 2011-06-28 |
* | Numbers: a particular case of div_unique | letouzey | 2011-06-24 |
* | Follow-up concerning eqb / ltb / leb comparisons | letouzey | 2011-06-21 |
* | Cleaning debugging printer relative to new proof engine. In | herbelin | 2011-06-21 |
* | Relaxed the constraint introduced in r14190 that froze the existing | herbelin | 2011-06-18 |
* | Fix bug 2269, program typechecker not used in Instance conclusions | msozeau | 2011-06-17 |
* | Tests de nsatz avec la geometrie | pottier | 2011-06-16 |
* | 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-10 |
* | 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-06-07 |
* | Check if recursive calls are guarded before printing "Proof completed". | herbelin | 2011-05-26 |
* | Q2R -> IQR | fbesson | 2011-05-25 |
* | Made the emacs-U option deprecated. Also removed the old code | courtieu | 2011-05-24 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0... | fbesson | 2011-05-23 |
* | added support to handle division by a constant over R | fbesson | 2011-05-20 |
* | 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-19 |
* | 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-18 |
* | Fixed my last patch: these files no longer use nat_beq (automatically | vsiles | 2011-05-16 |
* | A new mechanism to handle errors. | aspiwack | 2011-05-13 |
* | Print Module (Type) M now tries to print more details | letouzey | 2011-05-11 |
* | Improved lia + experimental nlia | fbesson | 2011-05-09 |
* | Additionnal fix of romega after modularisation of ZArith | letouzey | 2011-05-06 |
* | 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-05 |
* | First phase removing obsolete support for eta up to conversion in | herbelin | 2011-05-04 |
* | Fixed a bug causing inconsistent states during proof editting. | aspiwack | 2011-04-29 |
* | bug fix: concurrent access of persistent_cache | fbesson | 2011-04-21 |
* | Declarative mode: fix escape and return. | aspiwack | 2011-04-19 |
* | Extraction: nicer error when a toplevel module has no body (#2525) | letouzey | 2011-04-15 |