| Commit message (Expand) | Author | Age |
* | Refine patch for behavior of unify_to_subterm to allow backtracking on | Matthieu Sozeau | 2014-08-18 |
* | Remove confusing behavior of unify_with_subterm that could fail with | Matthieu Sozeau | 2014-08-14 |
* | Fix non-printing of coercions for primitive projections (fixes bug #3433). | Matthieu Sozeau | 2014-08-14 |
* | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | 2014-08-14 |
* | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau | 2014-08-13 |
* | Fix bug introduced by earlier commit on first-order unification of primitive | Matthieu Sozeau | 2014-08-10 |
* | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau | 2014-08-09 |
* | Allow pattern matching on the applied form of projections with primitive | Matthieu Sozeau | 2014-08-09 |
* | Do early occur-check in unification to allow eta to fire (fixes bug #3477) | Matthieu Sozeau | 2014-08-09 |
* | Using the asymmetric merging primitive in Evd. | Pierre-Marie Pédrot | 2014-08-09 |
* | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot | 2014-08-09 |
* | Tentative performance fix for Evd.merge_uctx. | Pierre-Marie Pédrot | 2014-08-09 |
* | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau | 2014-08-08 |
* | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | 2014-08-07 |
* | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | 2014-08-06 |
* | Small code simplification. | Pierre-Marie Pédrot | 2014-08-05 |
* | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin | 2014-08-05 |
* | - Fix handling of opaque polymorphic definitions which were turned transparent. | Matthieu Sozeau | 2014-08-03 |
* | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
* | - Fix has_undefined_evars not using its or_sorts argument anymore. | Matthieu Sozeau | 2014-08-03 |
* | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau | 2014-07-31 |
* | Avoid introducing additional universes when doing pruning in evarsolve. | Matthieu Sozeau | 2014-07-30 |
* | Rework code for refolding projections in whd_state/whd_simpl to allow Arguments | Matthieu Sozeau | 2014-07-29 |
* | Fix bug #3453, not recognizing primitive projections in Coercion declarations. | Matthieu Sozeau | 2014-07-29 |
* | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau | 2014-07-20 |
* | Fix coercion code to disallow using cumulativity in the domain of products, w... | Matthieu Sozeau | 2014-07-17 |
* | Add interface function to replace new_Type () | Matthieu Sozeau | 2014-07-14 |
* | Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo). | Matthieu Sozeau | 2014-07-10 |
* | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau | 2014-07-09 |
* | In flex-flex cases, the undefinedness of an evar can not be preseved after co... | Matthieu Sozeau | 2014-07-07 |
* | Missing check of evar instantiation, resulting in missing constraints (bug fr... | Matthieu Sozeau | 2014-07-07 |
* | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau | 2014-07-03 |
* | Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl... | Matthieu Sozeau | 2014-07-03 |
* | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau | 2014-07-03 |
* | Fix a Not_found anomaly raised by solve_evar_evar, we were breaking the | Matthieu Sozeau | 2014-07-02 |
* | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
* | Clarifying 'No such bound variable' message in apply, as suggested in #2387 | Hugo Herbelin | 2014-06-30 |
* | When building on-the-fly elimination principles, set the predicates universe ... | Matthieu Sozeau | 2014-06-29 |
* | Really honor the [simpl never] flag in whd_simpl, it was still doing reductio... | Matthieu Sozeau | 2014-06-29 |
* | Quick fix of bug #2996 continued (case of inductive types). | Hugo Herbelin | 2014-06-28 |
* | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin | 2014-06-28 |
* | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
* | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin | 2014-06-28 |
* | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | 2014-06-28 |
* | Small short optimization of instantiation in Evd. | Hugo Herbelin | 2014-06-28 |
* | Fast path in Canonical structure detection. We do not always compute the normal | Pierre-Marie Pédrot | 2014-06-27 |
* | Deactivate the "Standard Propositions Naming" flag, source of a lot of | Hugo Herbelin | 2014-06-26 |
* | Add an option to disable typeclass resolution during conversion, which | Matthieu Sozeau | 2014-06-26 |