| Age | Commit message (Expand) | Author |
|---|
| 2013-11-02 | Fixes parsing of all: followed by a typechecking/evaluation command. | aspiwack |
| 2013-11-02 | Adds a new goal selector "all:". | aspiwack |
| 2013-10-18 | declaration_hooks use Ephemeron | gareuselesinge |
| 2013-10-10 | STM: add "Stm Wait" to wait for the slaves to complete their jobs | gareuselesinge |
| 2013-10-07 | STM: new command "Stm PrintDag" to force printing the dag to /tmp | gareuselesinge |
| 2013-09-30 | STM: better handle proof modes | gareuselesinge |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-19 | Modulification and removing of structural equality in Stateid. | ppedrot |
| 2013-08-08 | stm: (initial) support for -coq-slaves | gareuselesinge |
| 2013-08-08 | get rid of closures in global/proof state | gareuselesinge |
| 2013-08-08 | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge |
| 2013-08-08 | Support Proof General | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-08-01 | Added a Print Debug GC command that displays the current state of | ppedrot |
| 2013-08-01 | Granting bug #3098: adding priority to Existing Instances. | ppedrot |
| 2013-07-17 | Declaremods: major refactoring, stop duplicating libobjects in modules | letouzey |
| 2013-07-17 | More dynamic argument scopes | letouzey |
| 2013-07-10 | Added a Register Inline command for the native compiler. Will be ported to th... | mdenes |
| 2013-07-09 | Revising r16550 about providing intro patterns for applying injection: | herbelin |
| 2013-06-27 | Getting rid of IntroPatternArgType. | ppedrot |
| 2013-06-27 | Removing useless tactic arguments, and using generic arguments | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-06 | More comments in Genarg. | ppedrot |
| 2013-06-05 | Replacing lists by maps in matching interpretation. | ppedrot |
| 2013-04-15 | More functional implementation of locality_flag and program_mode | gareuselesinge |
| 2013-03-13 | Modules and ppvernac, sequel of Enrico's commit 16261 | letouzey |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-10 | Useless use of hooks in VernacDefinition. In addition, this was | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-21 | Yet a new reduction tactic in Coq : cbn | pboutill |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Implemented a full-fledged equality on [constr_expr]. By the way, | ppedrot |
| 2012-10-31 | Change [Hints Resolve] to still accept constrs as arguments | msozeau |
| 2012-10-29 | Fixed #2926: | ppedrot |
| 2012-10-26 | Moved Entries module back to kernel | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-23 | Cleared a purely declarative .ml file and moved its interface to intf/ | ppedrot |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-10-06 | remove useless hidden_flag in TacMutual(Co)Fix | letouzey |
| 2012-10-06 | Tacexpr: revised version that doesn't need -rectypes | letouzey |
| 2012-10-04 | Moved Compat to parsing. This permits to break the dependency of the | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-10-02 | avoid referring to Term in constrexpr.mli and glob_term.mli | letouzey |
| 2012-10-01 | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu |
| 2012-08-24 | Correcting a comment in pattern-matching compilation. | aspiwack |
| 2012-08-11 | Added support for option Local (at module level) in Tactic Notation. | herbelin |
