aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-02-17Displaying environment and unfolding aliases in "cannot_unify"herbelin
2013-02-17A more informative message when the elimination predicate forherbelin
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2013-02-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
2013-02-10Moved code from Pretype_error to Evarutilppedrot
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Added backtrace information to anomaliesppedrot
2013-01-27Fixed bug #2967 (some missing check on ill-formed recursive notation strings).herbelin
2013-01-24Fixed parsing of -no-native-compiler flag.mdenes
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-19Array.create is deprecatedpboutill
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