| Age | Commit message (Expand) | Author |
|---|
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-29 | Not using a "cut" in descend_in_conjunctions induced more success. We | Hugo Herbelin |
| 2014-08-28 | Fixing an unnatural selection of subterms larger than expected in the | Hugo Herbelin |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross |
| 2014-08-25 | Fixing a bug introduced in the extension of 'apply in' + simplifying code. | Hugo Herbelin |
| 2014-08-18 | Fixing unification of subterms identified by patterns. | Hugo Herbelin |
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin |
| 2014-08-18 | Fix test-suite file. | Matthieu Sozeau |
| 2014-08-16 | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-07-11 | Fix Funind test-suite file after patch by Pierre. | Matthieu Sozeau |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-06-30 | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin |
| 2014-06-23 | Fix test-suite script for subst working with let-ins, the following proof was... | Matthieu Sozeau |
| 2014-06-23 | Changed syntax of explicit universes. | Matthieu Sozeau |
| 2014-06-08 | Fix canonical structure resolution in unification (bug found in Ssreflect). | Matthieu Sozeau |
| 2014-06-04 | - Better parsing and printing of named universes: Type{ident} and foo@{(ident... | Matthieu Sozeau |
| 2014-06-04 | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ...... | Hugo Herbelin |
| 2014-05-31 | Fixing introduction patterns * and ** when used in a branch so that they do n... | Hugo Herbelin |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin |
| 2014-05-06 | Comment in Funind.v test-suite file | Matthieu Sozeau |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | Fix restrict_universe_context removing some universes that do appear in the t... | Matthieu Sozeau |
| 2014-05-06 | Fix declarations of monomorphic assumptions | Matthieu Sozeau |
| 2014-05-06 | - Fix RecTutorial, and mutual induction schemes getting the wrong names. | Matthieu Sozeau |
| 2014-05-06 | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-26 | test for apply + TC resolution | Enrico Tassi |
| 2014-02-28 | Pos.compare_cont takes the comparison as first argument | Pierre Boutillier |
| 2014-01-06 | Add a test suite file for Ltac's "+" tactical. | Arnaud Spiwack |
| 2013-12-06 | Remove duplicate test-suite file. | Arnaud Spiwack |
| 2013-12-06 | Fix the refine related test-suite files to account for the new refine. | Arnaud Spiwack |
| 2013-09-03 | Fixing some tests from the test-suite. | ppedrot |
| 2013-09-02 | * test-suite/success/Unicode_utf8: | regisgia |
| 2013-07-17 | More dynamic argument scopes | letouzey |
| 2013-07-10 | Continuing r16621 on injection intro-patterns: | herbelin |
| 2013-07-09 | Revising r16550 about providing intro patterns for applying injection: | herbelin |
| 2013-06-10 | Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin... | msozeau |
| 2013-06-02 | Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an | herbelin |
| 2013-05-14 | Fixing a regression in unification introduced in r16205 (error raised | herbelin |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-05-08 | Declaration of multiple hypotheses or parameters now share typing | herbelin |
| 2013-05-08 | Share more information between constructors and arity of an inductive | herbelin |
| 2013-05-08 | Moved isolated test params_ind.v to Inductive.v. | herbelin |
| 2013-05-05 | Hack to solve a "Bad recursive type" anomaly. | herbelin |
| 2013-03-21 | Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in. | herbelin |
