aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* update of the file list in doc/stdlibGravatar letouzey2011-05-06
* BinNat: N.binary_rect is now a definition instead of an opaque proofGravatar letouzey2011-05-05
* Peano recursion for positive: integration of Daniel Schepler's codeGravatar letouzey2011-05-05
* Minimal lemmas about Z.gt, N.gt and coGravatar letouzey2011-05-05
* Modularisation of Znat, a few name changed elsewhereGravatar letouzey2011-05-05
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Modularization of NnatGravatar letouzey2011-05-05
* Setoid_ring: some cleanups related with BinPos and BinNatGravatar letouzey2011-05-05
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
* BinNatDef containing all functions of BinNat, misc adaptations in BinPosGravatar letouzey2011-05-05
* BinPosDef: a module with all code about positive, later Included in BinPosGravatar letouzey2011-05-05
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* Modularization of PnatGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
* Zdiv: results about eqm (the equality modulo some N) under a sectionGravatar letouzey2011-05-05
* Better comments and organisation in Datatypes.vGravatar letouzey2011-05-05
* Extraction: allow extraction foo when foo is an alias notationGravatar letouzey2011-05-05
* Fix merge, Cumul moved to CUMULGravatar msozeau2011-05-05
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
* First phase removing obsolete support for eta up to conversion inGravatar herbelin2011-05-04
* As many notation for for vectors as for List.Gravatar pboutill2011-05-03
* when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec.Gravatar pboutill2011-04-29
* Fixed a bug causing inconsistent states during proof editting.Gravatar aspiwack2011-04-29
* Some comments.Gravatar aspiwack2011-04-29
* Typo in test InitSyntax.outGravatar herbelin2011-04-29
* Choose relative directory over configured directory for coqlib.Gravatar pboutill2011-04-29
* Attempt to use more local doc in coqideGravatar pboutill2011-04-28
* CHANGES updateGravatar pboutill2011-04-28
* coq_makefile big cleanupGravatar pboutill2011-04-28
* coqtop -config returns coq returns coq environments at exection timeGravatar pboutill2011-04-28
* Revert r14078 "Partial backtrack on the support for open terms in destruct/in...Gravatar gmelquio2011-04-28
* Partial backtrack on the support for open terms in destruct/induction:Gravatar gmelquio2011-04-28
* Coqide: try to properly send interrupts to coqtop on Win32Gravatar letouzey2011-04-28
* Adding "Tactic Notation" in doc index.Gravatar herbelin2011-04-28
* Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedGravatar herbelin2011-04-28
* Fixed notation printing bug when curly brackets are involved (requestsGravatar herbelin2011-04-28
* Updating CHANGESGravatar herbelin2011-04-27
* Fixing output of Notations2.v test messed up in r14060Gravatar herbelin2011-04-27
* Pcoq.ml4: fix a typo in a comment to please ocamldocGravatar letouzey2011-04-26
* G_vernac can be parsed without grammar.cmaGravatar letouzey2011-04-26
* dev/base_include: no more mod_self_idGravatar letouzey2011-04-26
* Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).Gravatar herbelin2011-04-26
* Coqide: fix remove_current_view_page (#2499)Gravatar letouzey2011-04-26
* Fix for handling of -R "" in coqdoc (bug #2423).Gravatar herbelin2011-04-25
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
* Yet another bug in printing fix with let-in bindersGravatar herbelin2011-04-24
* Fixing bug in printing let-in binders in fix/cofixGravatar herbelin2011-04-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 05:24:20 +0000