| Commit message (Expand) | Author | Age |
* | Granting, undocumentedly, parsing of "Conjectures" as a synonym of | Hugo Herbelin | 2015-06-16 |
* | Add a [Redirect] vernacular command | Clément Pit--Claudel | 2015-05-04 |
* | Putting the From parameter of the Require command into the AST. | Pierre-Marie Pédrot | 2015-03-27 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Better doc and a few fixes for Proof using. | Enrico Tassi | 2014-12-19 |
* | Proof using: New vernacular to name sets of section variables | Enrico Tassi | 2014-12-18 |
* | About now accepts hypothesis names and goal selector. | Pierre Courtieu | 2014-12-15 |
* | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | 2014-12-12 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | Add [Info] command. | Arnaud Spiwack | 2014-11-01 |
* | Emit a warning for void Arguments statement (Close 3713) | Enrico Tassi | 2014-10-13 |
* | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin | 2014-09-30 |
* | Notation: option to attach extra pretty printing rules to notations | Enrico Tassi | 2014-09-29 |
* | Add syntax [id]: to apply tactic to goal named id. | Hugo Herbelin | 2014-09-12 |
* | Factorize the parsing rules of [Record] and the other kind of type definitions. | Arnaud Spiwack | 2014-09-04 |
* | Remove [Infer] option of records. | Arnaud Spiwack | 2014-09-04 |
* | Add a [Variant] declaration which allows to write non-recursive variant types. | Arnaud Spiwack | 2014-09-04 |
* | Fixing bug #3493. | Pierre-Marie Pédrot | 2014-08-27 |
* | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | 2014-08-05 |
* | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | 2014-08-05 |
* | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot | 2014-07-21 |
* | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
* | Fix bug #3289 | Matthieu Sozeau | 2014-06-11 |
* | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | Arnaud Spiwack | 2014-06-06 |
* | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Adding a Print Strategy vernacular command. It allows to check the | Pierre-Marie Pédrot | 2014-03-19 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Simpl_behaviour becomes Reductionops.ReductionBehaviour | Pierre Boutillier | 2014-02-24 |
* | Removing the [Require "file"] syntax. | Pierre-Marie Pédrot | 2014-02-02 |
* | Documenting old but useful command "Print Tables". | Hugo Herbelin | 2014-01-13 |
* | Fixing bug #3144. | Pierre-Marie Pédrot | 2014-01-10 |
* | Patch for supporting [From Xxx Require Yyy Zzz.] | Gregory Malecha | 2013-12-12 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | Fixes parsing of all: followed by a typechecking/evaluation command. | aspiwack | 2013-11-02 |
* | New option Default Goal Selector. | aspiwack | 2013-11-02 |
* | Adds a new goal selector "all:". | aspiwack | 2013-11-02 |
* | STM: add "Stm Wait" to wait for the slaves to complete their jobs | gareuselesinge | 2013-10-10 |
* | STM: new command "Stm PrintDag" to force printing the dag to /tmp | gareuselesinge | 2013-10-07 |
* | Modulification and removing of structural equality in Stateid. | ppedrot | 2013-08-19 |
* | Support Proof General | gareuselesinge | 2013-08-08 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | 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-08-01 |
* | More dynamic argument scopes | letouzey | 2013-07-17 |
* | Added a Register Inline command for the native compiler. Will be ported to th... | mdenes | 2013-07-10 |
* | Fixing warning of deprecated Argument Scopes. | ppedrot | 2013-05-28 |
* | Renaming SearchAbout into Search and Search into SearchHead. | herbelin | 2013-04-17 |
* | More functional implementation of locality_flag and program_mode | gareuselesinge | 2013-04-15 |
* | Modules and ppvernac, sequel of Enrico's commit 16261 | letouzey | 2013-03-13 |