aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove the unused "intel" field in Proof.proof_stateGravatar letouzey2012-10-02
* Remove some dead code in the vmGravatar letouzey2012-10-02
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Argextend: avoid useless "open Extrawit"Gravatar letouzey2012-10-02
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
* New makefile shortcuts miniopt and minibyte for coqtop + pluginsGravatar letouzey2012-10-02
* Use the library function List.substract in prev commitGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* Default hashconsing of identifiers.Gravatar ppedrot2012-09-27
* Reusing the Hashset data structure in Hashcons. Hopefully, this shouldGravatar ppedrot2012-09-26
* Incorrect commentGravatar msozeau2012-09-26
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* Fixing ocamldoc errorsGravatar ppedrot2012-09-25
* Added a ml-dot option to Makefile to generate dependency graph of core modulesGravatar ppedrot2012-09-25
* Fixing #2865.Gravatar ppedrot2012-09-25
* Fixing a bug introduced in Funind plugin when reorganizing the CListGravatar ppedrot2012-09-24
* Fix use of $(HASNATDYNLINK) in coq_makefile outputGravatar glondu2012-09-22
* Avoid generating ide/coqide_main*.ml as cleartext (except if READABLE_ML4 is ...Gravatar letouzey2012-09-20
* Remove broken makefile option NO_RECOMPILE_LIBGravatar letouzey2012-09-20
* Fixing Show Script issues.Gravatar ppedrot2012-09-20
* Coq_makefile fixupsGravatar pboutill2012-09-18
* More cleaning in CArray...Gravatar ppedrot2012-09-18
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* MacOS integration uses lablgtkosx >= 1.1Gravatar pboutill2012-09-17
* More type-safe interface to Coq XML API.Gravatar ppedrot2012-09-17
* Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen...Gravatar gmelquio2012-09-16
* Some more fixes to tactic documentation.Gravatar gmelquio2012-09-16
* Beautify tactic documentation a bit more.Gravatar gmelquio2012-09-16
* Remove superfluous spaces and commas in tactic documentation.Gravatar gmelquio2012-09-16
* Fix index generation for the pdf document.Gravatar gmelquio2012-09-16
* Fix failure to compile doc/stdlib/Library.tex.Gravatar gmelquio2012-09-15
* Port rewrites of tactic documentation from branch 8.4.Gravatar gmelquio2012-09-15
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Added some tricky tail-rec versions of List functions to CListGravatar ppedrot2012-09-14
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* lib/Pp:Gravatar regisgia2012-09-14
* kernel/Term:Gravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
* Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSGravatar pboutill2012-09-12
* Moved Pp to CLib. In particular, Pp does not depend on CAMLP4/5Gravatar ppedrot2012-09-10
* Fixed #2893.Gravatar ppedrot2012-09-10
* Added Print Assumptions command to CoqIDEGravatar ppedrot2012-09-10