aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-09-16Fix index generation for the pdf document.gmelquio
2012-09-15Fix failure to compile doc/stdlib/Library.tex.gmelquio
2012-09-15Port rewrites of tactic documentation from branch 8.4.gmelquio
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Added some tricky tail-rec versions of List functions to CListppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14lib/Pp:regisgia
2012-09-14kernel/Term:regisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
2012-09-12Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSpboutill
2012-09-10Moved Pp to CLib. In particular, Pp does not depend on CAMLP4/5ppedrot
2012-09-10Fixed #2893.ppedrot
2012-09-10Added Print Assumptions command to CoqIDEppedrot
2012-09-09When asked for a SearchAbout request, Coq now returns a more preciseppedrot
2012-09-09Fixed bug #2895ppedrot
2012-09-07Makefile: revised install-coqide ruleletouzey
2012-09-07Avoid [Loading ML file ...] messages when launching coqtopletouzey
2012-09-07Coqdoc: fix --utf8 bug for pretty printingpboutill
2012-09-06Added a comment/uncomment command to CoqIDEppedrot
2012-09-06Fix computation of obligations for mutually recursive definitions.msozeau
2012-09-06Nice output of SearchAbout command in CoqIDEppedrot
2012-09-05Obsolete syntax in documentation of Solve Obligation commands.ppedrot
2012-09-05Rationalized the behaviour of "Next Obligation" and "Admit Obligations"ppedrot
2012-09-05A few fixes in configure file:herbelin
2012-09-04Fix coqide compilation with lablgtk 2.16pboutill
2012-09-04Coqide Fix highlighting of Extraction, Import, Variablespboutill
2012-09-04test-suite: fix grep rule for output testspboutill
2012-09-04test-suite uses coqtop instead of coqtop.bytepboutill
2012-09-04Erase %.vo dependency to the phony target statespboutill
2012-08-24In the output tests, ignore dynlink messagesletouzey
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
2012-08-24Use fully-qualified Coq.Init.Prelude when starting coqtopletouzey
2012-08-24Fix Extraction Implicit on axioms.aspiwack
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-24Better highlighting of strings in coqide.aspiwack
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
2012-08-24Modification of the unjustified tag.aspiwack
2012-08-24Correcting a comment in pattern-matching compilation.aspiwack
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
2012-08-23CHANGES: document the end of states/initial.coq and coqtop.optletouzey
2012-08-23Remove a script unused since 2006 (cf commit r8626)letouzey
2012-08-23myocamlbuild : fixes for new printing directory + sourceview for coqideletouzey
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
2012-08-23No need anymore to refer to COQLIB in ocamldebug-coqletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 12:43:36 +0000