| Age | Commit message (Expand) | Author |
|---|
| 2015-03-03 | Add a test-suite file ensuring coinductives with primitive projections | Matthieu Sozeau |
| 2015-02-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-02-27 | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin |
| 2015-02-24 | Other tests for decl mode, coming from reference manual. | Hugo Herbelin |
| 2015-02-23 | Fixing rewrite/subst when the subterm to rewrite is argument of an Evar. | Hugo Herbelin |
| 2015-02-23 | Fixing occur-check which was too strong in unification.ml. | Hugo Herbelin |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi |
| 2015-02-11 | Adding a test-suite for tactic notation naming. | Pierre-Marie Pédrot |
| 2015-01-17 | Revert "Fix files in test-suite having to do with Require inside modules." | Maxime Dénès |
| 2015-01-17 | Univs: Fix alias computation for VMs, computation of normal form of | Matthieu Sozeau |
| 2015-01-12 | Fix files in test-suite having to do with Require inside modules. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-11 | Extraction: discard code unnecessary to fulfill a module signature | Pierre Letouzey |
| 2015-01-01 | An optimization in the use of unification candidates so as to get the | Hugo Herbelin |
| 2014-12-19 | Better doc and a few fixes for Proof using. | Enrico Tassi |
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi |
| 2014-12-16 | fix bug #2447 in congruence | Pierre Corbineau |
| 2014-12-10 | Fixing orientation of postponed subtyping problems. | Hugo Herbelin |
| 2014-12-07 | Improving evar restriction (this is a risky change, as I remember a | Hugo Herbelin |
| 2014-12-04 | Take benefit of improved name preservation of evars in e2fa65fcc. | Hugo Herbelin |
| 2014-12-02 | When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if | Hugo Herbelin |
| 2014-11-25 | Adapting to current semantics of "simpl non-evaluable-cst" | Hugo Herbelin |
| 2014-11-25 | Experimenting using unification when matching evar/meta free subterms | Hugo Herbelin |
| 2014-11-22 | Add test-suite file for dependent rewriting example by Vadim Zaliva and | Matthieu Sozeau |
| 2014-11-18 | Fixing a little bug with nested but convertible occurrences in "destruct at". | Hugo Herbelin |
| 2014-11-18 | Fixing detection of occurrences in the presence of nested subterms for | Hugo Herbelin |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin |
| 2014-11-16 | Fixing side bug in db37c9f3f32ae7 delaying interpretation of the | Hugo Herbelin |
| 2014-11-14 | Preserving the good effect of 014e5ac92a on not leaving dangling local | Hugo Herbelin |
| 2014-11-13 | Removing yet another source of remaining local definitions. | Hugo Herbelin |
| 2014-11-08 | Follow up to experimental eager evar unification in bcba6d1bc9: | Hugo Herbelin |
| 2014-11-08 | Compatibility with 8.4 in the heuristic used to build the induction | Hugo Herbelin |
| 2014-11-06 | Restoring clear_flag (thanks a lot to jonikelee to notice it). | Hugo Herbelin |
| 2014-11-06 | Optimizing when to clear generalized hypotheses in destruct. | Hugo Herbelin |
| 2014-11-06 | Removing "destruct" test not yet working. | Hugo Herbelin |
| 2014-11-03 | Subtle swap of lines to preserve VarInstance src field before checking | Hugo Herbelin |
| 2014-11-03 | Fix to 844431761 on improving elimination with indices, getting rid of | Hugo Herbelin |
| 2014-11-02 | Improving elimination with indices, getting rid of intrusive residual | Hugo Herbelin |
| 2014-11-02 | Some reorganization of the code for destruct/induction: | Hugo Herbelin |
| 2014-11-02 | Fixing file destruct.v. | Hugo Herbelin |
| 2014-10-31 | Enlarge the cases where the like first selection is used in destruct. | Hugo Herbelin |
| 2014-10-31 | Listing a few examples of destruct showing unsatisfactory behaviors. | Hugo Herbelin |
| 2014-10-31 | Avoid "destruct H" to apply on H itself when H is a section variable. | Hugo Herbelin |
| 2014-10-27 | Making destruct on idents with maximal implicit arguments working, by | Hugo Herbelin |
| 2014-10-27 | Ensuring compatibility when an hypothesis used for destruct is | Hugo Herbelin |
| 2014-10-27 | Fixing clash in test destruct.v. | Hugo Herbelin |
| 2014-10-26 | Fixing destruct/induction with a using clause on a non-inductive type, | Hugo Herbelin |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-22 | Fixing an evar leak in pattern-matching compilation (#3758). | Hugo Herbelin |
| 2014-10-20 | Fixing a bug in the presence of let-in in inductive arity. | Hugo Herbelin |
