aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Modulification of LabelGravatar ppedrot2012-12-18
* Ide_slave: do not prepare debug messages in non-debug modeGravatar letouzey2012-12-17
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
* Using library string functions.Gravatar ppedrot2012-12-13
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
* Restoring flush of Welcome message lost in r15148Gravatar herbelin2012-12-06
* Removed Compat.Exc_located outside of compat.ml4, as a consequence ofGravatar herbelin2012-12-04
* Low-level hack to get some more informative message from dynamic loading errors.Gravatar herbelin2012-12-04
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* Print Assumptions: restore a final \nGravatar letouzey2012-11-17
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* backtrack too much commited files in the last commit.Gravatar courtieu2012-11-15
* Fixing emacs diff bug with .dir-locals.el.Gravatar courtieu2012-11-15
* Added a CString module.Gravatar ppedrot2012-11-13
* Another GC testGravatar ppedrot2012-11-13
* Ide_slave: do not attempt to answer broken requestsGravatar letouzey2012-11-12
* Xml_parser: detect immediate EOF + disable check_eof by defaultGravatar letouzey2012-11-12
* Removed the modification of the GC pressure coefficient, in orderGravatar ppedrot2012-11-12
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Coq is a heavy user of persistent data structures and symbolic ASTs, so theGravatar ppedrot2012-11-06
* Fixed #2926:Gravatar ppedrot2012-10-29
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Text inserted by insert_this_phrase_on_success correct taggingGravatar pboutill2012-10-23
* Fix test-suite output/* in benchGravatar pboutill2012-10-17
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* When loading a plugin, prefer .cma to .cmoGravatar gareuselesinge2012-10-14
* Turn mltop.ml4 into a regular ocaml fileGravatar letouzey2012-10-06
* still some more dead code removalGravatar letouzey2012-10-06
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* coqtop -time : display per-command timingsGravatar letouzey2012-10-05
* Improving error message when abtraction over goal (abstract_list_allGravatar herbelin2012-10-04
* Adding a nominal typing layer to Metasyntax in order to clarifyGravatar ppedrot2012-10-04
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Fixing #2865.Gravatar ppedrot2012-09-25
* More cleaning in CArray...Gravatar ppedrot2012-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
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15