aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-17Ide_slave: do not prepare debug messages in non-debug modeletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-12-13Using library string functions.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-08Ensure that a function declared with a label is used with itletouzey
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-12-06Restoring flush of Welcome message lost in r15148herbelin
2012-12-04Removed Compat.Exc_located outside of compat.ml4, as a consequence ofherbelin
2012-12-04Low-level hack to get some more informative message from dynamic loading errors.herbelin
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-17Print Assumptions: restore a final \nletouzey
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-11-15backtrack too much commited files in the last commit.courtieu
2012-11-15Fixing emacs diff bug with .dir-locals.el.courtieu
2012-11-13Added a CString module.ppedrot
2012-11-13Another GC testppedrot
2012-11-12Ide_slave: do not attempt to answer broken requestsletouzey
2012-11-12Xml_parser: detect immediate EOF + disable check_eof by defaultletouzey
2012-11-12Removed the modification of the GC pressure coefficient, in orderppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-11-06Coq is a heavy user of persistent data structures and symbolic ASTs, so theppedrot
2012-10-29Fixed #2926:ppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-23Text inserted by insert_this_phrase_on_success correct taggingpboutill
2012-10-17Fix test-suite output/* in benchpboutill
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-14When loading a plugin, prefer .cma to .cmogareuselesinge
2012-10-06Turn mltop.ml4 into a regular ocaml fileletouzey
2012-10-06still some more dead code removalletouzey
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-05coqtop -time : display per-command timingsletouzey
2012-10-04Improving error message when abtraction over goal (abstract_list_allherbelin
2012-10-04Adding a nominal typing layer to Metasyntax in order to clarifyppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-25Fixing #2865.ppedrot
2012-09-18More cleaning in CArray...ppedrot
2012-09-18Cleaning interface of Util.ppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot