| Commit message (Expand) | Author | Age |
* | Print Assumptions: restore a final \n | letouzey | 2012-11-17 |
* | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
* | Fixed #2926: | ppedrot | 2012-10-29 |
* | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey | 2012-10-16 |
* | Fixing #2865. | ppedrot | 2012-09-25 |
* | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot | 2012-09-14 |
* | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot | 2012-09-14 |
* | This patch removes unused "open" (automatically generated from | regisgia | 2012-09-14 |
* | Assumption commands are now displayed as unsafe in Coqide. | aspiwack | 2012-08-24 |
* | Do not forget to build the unicode libraries, necessary to compile and launch... | msozeau | 2012-08-22 |
* | Added support for option Local (at module level) in Tactic Notation. | herbelin | 2012-08-11 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Vecnacentries.dump_global silently ignores exceptions | pboutill | 2012-08-06 |
* | Dump references in reduction tactics | pboutill | 2012-08-05 |
* | Dump references in Reset | pboutill | 2012-08-05 |
* | Fixing test-suite | pboutill | 2012-07-20 |
* | Various minor fixes to coqdoc from A. Chlipala. | msozeau | 2012-07-18 |
* | A new status Unsafe in Interface. Meant for commands such as Admitted. | aspiwack | 2012-07-12 |
* | Vernacentries: minor code cleanup | letouzey | 2012-07-12 |
* | Also allow Reset in Load'ed files | letouzey | 2012-07-11 |
* | Re-allow Reset in compiled files | letouzey | 2012-07-11 |
* | Fixes bug 2841 ([Focus 0] gives anomaly). | aspiwack | 2012-07-10 |
* | Restore an indentation of Show Script | letouzey | 2012-07-07 |
* | A prototype implementation of a Print Namespace command. | aspiwack | 2012-07-06 |
* | Backtrack: add support for the "Proof c." syntax (fix #2832) | letouzey | 2012-07-06 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | I forgot a line in previous commit. | aspiwack | 2012-06-22 |
* | A call to the command Proof (and its variants) now prints the subgoals. | aspiwack | 2012-06-22 |
* | Getting rid of Pcoq remains. | ppedrot | 2012-06-12 |
* | Separated notice vs info messages, and cleaned up the interface a bit. | ppedrot | 2012-06-04 |
* | More cleaning | ppedrot | 2012-06-01 |
* | Cleaning Pp.ppnl use | ppedrot | 2012-06-01 |
* | Getting rid of Pp.msgnl and Pp.message. | ppedrot | 2012-06-01 |
* | Getting rid of Pp.msg | ppedrot | 2012-05-30 |
* | More uniformisation in Pp.warn functions. | ppedrot | 2012-05-30 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | Stuff about notation_constr (ex-aconstr) now in notation_ops.ml | letouzey | 2012-05-29 |
* | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey | 2012-05-29 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
* | Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml | letouzey | 2012-05-29 |
* | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey | 2012-05-29 |
* | Program: avoid staying in program mode after a failed Program command | letouzey | 2012-04-26 |
* | correct abort in Function when a proof of inversion fails | letouzey | 2012-04-23 |
* | Corrects a (very) longstanding bug of tactics. As is were, tactic expecting | aspiwack | 2012-04-18 |
* | lib directory is cut in 2 cma. | pboutill | 2012-04-12 |
* | Added a command "Unfocused" which returns an error when the proof is | aspiwack | 2012-03-30 |
* | Slight change in the semantics of arguments scopes: scopes can no | herbelin | 2012-03-26 |
* | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey | 2012-03-23 |
* | Remove undocumented command "Delete foo" | letouzey | 2012-03-23 |
* | Remove old proof-managment commands Suspend/Resume | letouzey | 2012-03-23 |