| Age | Commit message (Expand) | Author |
|---|
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-10-07 | Test for record syntax parsing. | Pierre-Marie Pédrot |
| 2015-10-07 | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau |
| 2015-09-16 | In pat/constr introduction patterns, fixing in a better way clearing problems | Hugo Herbelin |
| 2015-09-08 | Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits | Hugo Herbelin |
| 2015-09-08 | Ensuring that patterns of the form pat/constr move the hypotheses replacing | Hugo Herbelin |
| 2015-08-02 | Continuing 817308ab (use ltac env for terms in ltac context) + fix | Hugo Herbelin |
| 2015-08-02 | Fixing test apply.v (had wrong option name). | Hugo Herbelin |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Fixing test apply.v (had wrong option name). | Hugo Herbelin |
| 2015-08-02 | Fixing #4221 (interpreting bound variables using ltac env was possibly | Hugo Herbelin |
| 2015-08-02 | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin |
| 2015-07-22 | Extraction: fix primitive projection extraction. | Matthieu Sozeau |
| 2015-07-07 | Univs: bug fix. | Matthieu Sozeau |
| 2015-06-28 | Fix incompleteness of conversion used by evarconv | Matthieu Sozeau |
| 2015-06-23 | Fixing incompatibility introduced with simpl in commit 364decf59c1 (or | Hugo Herbelin |
| 2015-05-12 | Extraction: fix the detection of the "polyprop" situation | Pierre Letouzey |
| 2015-05-09 | Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default). | Hugo Herbelin |
| 2015-05-06 | Fixing treatment of recursive equations damaged by 857e82b2ca0d1. | Hugo Herbelin |
| 2015-04-01 | Fixing test-suite. | Pierre-Marie Pédrot |
| 2015-03-25 | Fully fixing bug #3491 (anomaly when building _rect scheme in the | Hugo Herbelin |
| 2015-03-25 | Another example about the consequence of a wrong computation of the | Hugo Herbelin |
| 2015-03-24 | Fixing computation of non-recursively uniform arguments in the | Hugo Herbelin |
| 2015-03-24 | Fixing wrong rel_context in checking positivity condition. | Hugo Herbelin |
| 2015-03-22 | Qed export -> Qed exporting | Enrico Tassi |
| 2015-03-13 | Add some tests for tryif | Jason Gross |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-03-03 | Add a test-suite file ensuring coinductives with primitive projections | Matthieu Sozeau |
| 2015-02-27 | Fixing first part of bug #3210 (inference of pattern-matching return | 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 |
