| Commit message (Expand) | Author | Age |
* | 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 |
* | 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-03-11 |
* | Useless use of hooks in VernacDefinition. In addition, this was | ppedrot | 2013-02-10 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Monomorphization (parsing) | ppedrot | 2012-11-25 |
* | Fixed #2926: | ppedrot | 2012-10-29 |
* | Moved Compat to parsing. This permits to break the dependency of the | ppedrot | 2012-10-04 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | Added support for option Local (at module level) in Tactic Notation. | herbelin | 2012-08-11 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Re-allow Reset in compiled files | letouzey | 2012-07-11 |
* | A prototype implementation of a Print Namespace command. | aspiwack | 2012-07-06 |
* | Notation: a new annotation "compat 8.x" extending "only parsing" | letouzey | 2012-07-05 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Added a color output to Coqtop. | ppedrot | 2012-06-04 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey | 2012-05-29 |
* | Migrate the grammar entry about "Ltac" into g_vernac.ml4. | letouzey | 2012-05-29 |
* | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey | 2012-05-29 |
* | Glob_term now mli-only, operations now in Glob_ops | letouzey | 2012-05-29 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | 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 |
* | Slight change in the semantics of arguments scopes: scopes can no | herbelin | 2012-03-26 |
* | Remove undocumented command "Delete foo" | letouzey | 2012-03-23 |
* | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau | 2012-03-14 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Arguments supports extra notation scopes | gareuselesinge | 2012-02-14 |
* | Fix camlp4 compilation | pboutill | 2012-01-31 |
* | Added an pattern / occurence syntax for vm_compute. | ppedrot | 2012-01-30 |
* | Removed a seemingly unused argument in Require of modules, introduced 10 year... | ppedrot | 2012-01-23 |
* | Reverted previous commit, which broke library compilation. | ppedrot | 2012-01-20 |