| Commit message (Expand) | Author | Age |
* | 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 |
* | This is a quick hack to permit the parsing of the locality flag in the Progra... | ppedrot | 2012-01-20 |
* | Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}. | msozeau | 2012-01-19 |
* | A pass on warning printings. Made systematic the use of msg_warning so | herbelin | 2011-12-17 |
* | Fixing previous commit which was bugging on tactics preceded by goal number (... | courtieu | 2011-12-16 |
* | Moving bullets (-, +, *) into stand-alone commands instead of being | courtieu | 2011-12-16 |
* | Minor fixes to Arguments | gareuselesinge | 2011-12-06 |
* | Continuing r14747 being actually incomplete (flushing warnings and | herbelin | 2011-11-30 |
* | Preventing Implicit Arguments warning to be shown in non verbose mode | herbelin | 2011-11-30 |
* | New Arguments vernacular | gareuselesinge | 2011-11-21 |
* | Adding the type infrastructure to handle properly API management of options | ppedrot | 2011-11-18 |
* | Fix parsing of :>> and backtrack correctly on the cache of hints for local co... | msozeau | 2011-11-18 |
* | Restore backward compatibility. ":>" declares subinstances in Class declarati... | msozeau | 2011-11-18 |
* | Merge subinstances branch by me and Tom Prince. | msozeau | 2011-11-17 |
* | Quick improvement of some error messages related to module application | herbelin | 2011-08-30 |
* | Adding a new syntax for BeginSubproof and EndSubproof, namely { and }. | courtieu | 2011-07-05 |
* | Break circular dependency Proof_global -> Vernacexpr -> Proof_global. | aspiwack | 2011-05-17 |
* | New option [Set Bullet Behavior] allows to select the behaviour of bullets. | aspiwack | 2011-05-13 |
* | G_vernac can be parsed without grammar.cma | letouzey | 2011-04-26 |