| Age | Commit message (Expand) | Author |
|---|
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-11-10 | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | ppedrot |
| 2013-11-09 | Revert the previous commit. It broke Coq compilation. | ppedrot |
| 2013-11-09 | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | ppedrot |
| 2013-11-05 | STM: fix for PG and "Proof term" lines. | gareuselesinge |
| 2013-11-02 | Adds an experimental exactly_once tactical. | aspiwack |
| 2013-11-02 | Adds a tactical once. | aspiwack |
| 2013-11-02 | Added the tactical "tac1 + tac2". | aspiwack |
| 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 |
