aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-05-05Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)letouzey
2011-05-05BinNatDef containing all functions of BinNat, misc adaptations in BinPosletouzey
2011-05-05BinPosDef: a module with all code about positive, later Included in BinPosletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
2011-05-05Modularization of Pnatletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2011-05-05Zdiv: results about eqm (the equality modulo some N) under a sectionletouzey
2011-05-05Better comments and organisation in Datatypes.vletouzey
2011-05-05Extraction: allow extraction foo when foo is an alias notationletouzey
2011-05-05Fix merge, Cumul moved to CUMULmsozeau
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
2011-05-03As many notation for for vectors as for List.pboutill
2011-04-29when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec.pboutill
2011-04-29Fixed a bug causing inconsistent states during proof editting.aspiwack
2011-04-29Some comments.aspiwack
2011-04-29Typo in test InitSyntax.outherbelin
2011-04-29Choose relative directory over configured directory for coqlib.pboutill
2011-04-28Attempt to use more local doc in coqidepboutill
2011-04-28CHANGES updatepboutill
2011-04-28coq_makefile big cleanuppboutill
2011-04-28coqtop -config returns coq returns coq environments at exection timepboutill
2011-04-28Revert r14078 "Partial backtrack on the support for open terms in destruct/in...gmelquio
2011-04-28Partial backtrack on the support for open terms in destruct/induction:gmelquio
2011-04-28Coqide: try to properly send interrupts to coqtop on Win32letouzey
2011-04-28Adding "Tactic Notation" in doc index.herbelin
2011-04-28Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedherbelin
2011-04-28Fixed notation printing bug when curly brackets are involved (requestsherbelin
2011-04-27Updating CHANGESherbelin
2011-04-27Fixing output of Notations2.v test messed up in r14060herbelin
2011-04-26Pcoq.ml4: fix a typo in a comment to please ocamldocletouzey
2011-04-26G_vernac can be parsed without grammar.cmaletouzey
2011-04-26dev/base_include: no more mod_self_idletouzey
2011-04-26Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).herbelin
2011-04-26Coqide: fix remove_current_view_page (#2499)letouzey
2011-04-25Fix for handling of -R "" in coqdoc (bug #2423).herbelin
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-24Yet another bug in printing fix with let-in bindersherbelin
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions behi...herbelin
2011-04-22Coqide: fix synchro when restarting during a single stepletouzey
2011-04-21Coqide: let's try to be synchronuous when killing coqtopletouzey
2011-04-21Coqide: remove some dead codeletouzey
2011-04-21Coqlib: avoid deadlock under win32 with force_reset_initialletouzey
2011-04-21Coqide: back to using Unix.stderr in create_processletouzey
2011-04-21Coqide: better handling of stdout/stderr in win32letouzey
2011-04-21Coqide: typoletouzey
2011-04-21Coqide: quote coqtop filename if necessaryletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 23:05:09 +0000