aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
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-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-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
2012-09-10Fixed #2893.ppedrot
2012-09-09When asked for a SearchAbout request, Coq now returns a more preciseppedrot
2012-09-07Avoid [Loading ML file ...] messages when launching coqtopletouzey
2012-09-06Fix computation of obligations for mutually recursive definitions.msozeau
2012-09-05Rationalized the behaviour of "Next Obligation" and "Admit Obligations"ppedrot
2012-08-24Use fully-qualified Coq.Init.Prelude when starting coqtopletouzey
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
2012-08-22Do not forget to build the unicode libraries, necessary to compile and launch...msozeau
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
2012-08-05Dump references in reduction tacticspboutill
2012-08-05Dump references in Resetpboutill
2012-07-20Fixing test-suitepboutill
2012-07-20Let coqtop be a little more stupid in hint answer: otherwise, thatppedrot
2012-07-18Various minor fixes to coqdoc from A. Chlipala.msozeau
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
2012-07-12Ensure that a plugin init function is called only onceletouzey
2012-07-12Vernacentries: minor code cleanupletouzey
2012-07-12Bug 2838: ExplApp in mutual inductive parameterspboutill
2012-07-11Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820letouzey
2012-07-11Also allow Reset in Load'ed filesletouzey
2012-07-11Re-allow Reset in compiled filesletouzey
2012-07-11Fix typeclass error handling which was sometimes raising a Failure ("hd").msozeau
2012-07-10Adapting the IDE interface with the focussed display.ppedrot
2012-07-10Fixes bug 2841 ([Focus 0] gives anomaly).aspiwack
2012-07-09Moved code out of ide_slave in a more appropriate place.ppedrot
2012-07-08verbose compat notations : nicer option nameletouzey
2012-07-07Restore an indentation of Show Scriptletouzey
2012-07-06A prototype implementation of a Print Namespace command.aspiwack
2012-07-06Backtrack: add support for the "Proof c." syntax (fix #2832)letouzey
2012-07-05rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 07:11:38 +0000