| Age | Commit message (Expand) | Author |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-06-29 | A new infrastructure for warnings. | Maxime Dénès |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-11-19 | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau |
| 2015-04-22 | Fixing non exhaustive pattern-matching. | Hugo Herbelin |
| 2015-04-21 | Fixing #3383 (a "return" clause without an "in" clause is not enough | Hugo Herbelin |
| 2015-04-09 | Really fix constr_of_pattern and bugs #3590 and #4120 by | Matthieu Sozeau |
| 2015-04-09 | Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic... | Matthieu Sozeau |
| 2015-03-03 | Fix bug #3590, keeping evars that are not turned into named metas by | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin |
| 2014-10-03 | Fixing #3623 (unbound evars in types in a call to "change with"). | Hugo Herbelin |
| 2014-10-02 | Completing fixing order of parameters when translating from | Hugo Herbelin |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-27 | Make pattern_of_constr typed so that we can infer the proper patterns | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-19 | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-08 | Parsing of Type@{max(i,j)}. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 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-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-01 | Fixing #3088. Translation from globconstrs to patterns was forgetting | ppedrot |
| 2013-06-05 | Replacing lists by maps in matching interpretation. | ppedrot |
| 2013-05-08 | Uniformizing the [if_warn] flag used for warning printing and put | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-12-13 | Renamed Option.Misc.compare to the more uniform Option.equal. | ppedrot |
| 2012-11-23 | Added a constr_pattern_eq | ppedrot |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Pattern as a mli-only file, operations in Patternops | letouzey |