| Age | Commit message (Expand) | Author |
|---|
| 2016-07-03 | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) | Pierre Letouzey |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-07-01 | Separate flags for fix/cofix/match reduction and clean reduction function names. | Maxime Dénès |
| 2016-02-15 | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik |
| 2016-02-15 | Using monotonic types for conversion functions. | Pierre-Marie Pédrot |
| 2016-02-15 | Monotonizing the Evarutil module. | Pierre-Marie Pédrot |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2015-05-13 | Safer typing primitives. | Pierre-Marie Pédrot |
| 2015-02-15 | Fix 'don't expose cases' in cbn | Pierre Boutillier |
| 2015-02-15 | Fixing bug #3490. | Pierre-Marie Pédrot |
| 2015-02-15 | Fixing bug #3916. | Pierre-Marie Pédrot |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin |
| 2014-11-18 | Fixing detection of occurrences in the presence of nested subterms for | Hugo Herbelin |
| 2014-11-02 | Cosmetic changes. | Hugo Herbelin |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-24 | Change reduction_of_red_expr to return an e_reduction_function returning | Matthieu Sozeau |
| 2014-10-15 | Fix bug 3637. | Matthieu Sozeau |
| 2014-10-10 | Fix bug due to shadowing a variable name in tacred | Matthieu Sozeau |
| 2014-09-27 | Fix semantics of matching with folded/unfolded projections to definitely | Matthieu Sozeau |
| 2014-09-27 | Fix bug 3662 by actually reducing primitive projections in cbv/compute. | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-24 | Return a Prop not an arbitrary Type, and correct a typo. | Matthieu Sozeau |
| 2014-09-24 | Make eq_pattern_test/eq_test work up to the equivalence of primitive | Matthieu Sozeau |
| 2014-09-23 | Fix bug #3656. | Matthieu Sozeau |
| 2014-09-19 | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau |
| 2014-09-19 | Fixing #3641 (loop in e_contextually, introduced in r16525). | Hugo Herbelin |
| 2014-09-19 | Revert change of e_contextually as it needlessly expands all primitive | Matthieu Sozeau |
| 2014-09-18 | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-11 | Fix bug #3596, wrong treatment of projections in compute_constelim_direct. | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-29 | Rework code for refolding projections in whd_state/whd_simpl to allow Arguments | Matthieu Sozeau |
| 2014-06-29 | Really honor the [simpl never] flag in whd_simpl, it was still doing reductio... | Matthieu Sozeau |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 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-04 | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin |
| 2014-05-26 | Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q | Pierre Boutillier |
| 2014-05-26 | Reduction.Stack.Fix/Case stores Cst_stack.t | Pierre Boutillier |
