| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2013-03-30 | Continuation of r16346 on filtering local definitions. Refined | herbelin |
| 2013-03-25 | Fix bug #2989: make unification.ml able to deal with canonical structure in a... | pboutill |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey |
| 2013-03-05 | More monomorphization. | ppedrot |
| 2013-02-28 | compare_stack_shape before ise_stack2 in evar_conv | pboutill |
| 2013-02-28 | Repairing r16205: errors raised by check_evar_instance were no longer | herbelin |
| 2013-02-25 | Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo... | pboutill |
| 2013-02-17 | A more informative message when the elimination predicate for | herbelin |
