| Age | Commit message (Expand) | Author |
|---|
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-28 | There are some occurs-check cases that can be handled by imitation (using pru... | Matthieu Sozeau |
| 2014-08-26 | Make evarconv and unification able to handle eta for records in presence | Matthieu Sozeau |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau |
| 2014-08-14 | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau |
| 2014-08-10 | Fix bug introduced by earlier commit on first-order unification of primitive | Matthieu Sozeau |
| 2014-08-09 | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau |
| 2014-08-08 | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau |
| 2014-07-09 | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau |
| 2014-07-07 | In flex-flex cases, the undefinedness of an evar can not be preseved after co... | Matthieu Sozeau |
| 2014-07-03 | Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl... | Matthieu Sozeau |
| 2014-06-25 | Use full transparent state when checking well-typedness of a second order mat... | Matthieu Sozeau |
| 2014-06-17 | Reinstate eta for records in evarconv, fixing two HoTT coq bugs. | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-16 | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau |
| 2014-06-13 | Adapt simpl/cbn unfolding and refolding machinery to projections, so that | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-08 | Fix canonical structure resolution in unification (bug found in Ssreflect). | Matthieu Sozeau |
| 2014-06-04 | Fix canonical structure resolution (makes test-suite files go through again). | Matthieu Sozeau |
| 2014-05-16 | More fixes of unification with primitive projections (missed cases during the... | Matthieu Sozeau |
| 2014-05-16 | Fix unification of non-unfoldable primitive projections in evarconv. | Matthieu Sozeau |
| 2014-05-09 | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau |
| 2014-05-06 | - Add back some compatibility functions to avoid rewriting plugins. | Matthieu Sozeau |
| 2014-05-06 | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau |
| 2014-05-06 | In case two constants/vars/rels are _not_ defined, force unification of unive... | Matthieu Sozeau |
| 2014-05-06 | - Fix comparison of universes. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-01 | Propagating conversion_problem towards (postponed) evar/evar problems. | Hugo Herbelin |
| 2014-03-17 | Evarconv: exact_ise_stack looks to stack head before bodies or branches | Pierre Boutillier |
| 2014-03-16 | consider_remaining_unif_problems respects Conv_oracle | Pierre Boutillier |
| 2014-03-10 | Evarconv unification respects Conv_oracle | Pierre Boutillier |
| 2014-03-10 | MaybeFlexible semantic changes | Pierre Boutillier |
| 2014-02-24 | Create Debug Unification option | Pierre Boutillier |
| 2014-02-24 | No more translation array <-> list in Reductionops.Stack | Pierre Boutillier |
| 2014-02-24 | Reductionops.Stack.strip* are ready to deal with Shift | Pierre Boutillier |
| 2014-02-24 | Reductionops.Stack.app_node is secret | Pierre Boutillier |
| 2014-02-24 | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier |
| 2013-10-27 | Abstracting evar filter away. The API is not perfect, but better than nothing. | ppedrot |
| 2013-10-23 | Small optimizations in unification. | ppedrot |
| 2013-10-22 | Removing useless array-to-list and converse casts used in | ppedrot |
| 2013-10-22 | Optimizing evar filters. It seems to cost quite a lot in unification, | ppedrot |
| 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-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-05-30 | Do not compute fallback eagerly in Evarconv | pboutill |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-05-06 | Small cleaning of Evd interface. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-17 | Fix of r16257 in r16205 for "errors raised by check_evar_instance were | herbelin |
| 2013-04-17 | Like in r16346, do not filter local definitions (here in the | herbelin |
