| Age | Commit message (Expand) | Author |
|---|
| 2016-08-09 | Reduce warning noise when compiling the standard library. | Guillaume Melquiond |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-06-08 | Compilation via pack for plugins of the stdlib | Pierre Letouzey |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-05-16 | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot |
| 2016-03-17 | Removing the special status of generic entries defined by Coq itself. | Pierre-Marie Pédrot |
| 2016-03-04 | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot |
| 2016-02-24 | Getting rid of the "<:tactic< ... >>" quotations. | Pierre-Marie Pédrot |
| 2016-02-15 | Moving conversion functions to the new tactic API. | Pierre-Marie Pédrot |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-12-07 | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | Clean up a comment in plugins/romega/ReflOmegaCore | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-06-23 | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-10-23 | cList.index is now cList.index_f, same for index0 | letouzey |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 15) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 11) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 7) | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2012-12-18 | No more constant named "int" in Coq theories (cf bug #2878) | letouzey |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-06-01 | Cleaning Pp.ppnl use | ppedrot |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
