| Commit message (Expand) | Author | Age |
* | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | 2015-12-02 |
* | Fixing the "parsing rules with idents later declared as keywords" problem. | Hugo Herbelin | 2015-11-26 |
* | Fixing a vm_compute bug in the presence of let-ins among the | Hugo Herbelin | 2015-11-22 |
* | Fixing a bug of adjust_subst_to_rel_context. | Hugo Herbelin | 2015-11-22 |
* | Fixing kernel bug in typing match with let-ins in the arity. | Hugo Herbelin | 2015-11-22 |
* | Fixing logical bugs in the presence of let-ins in computiong primitive | Hugo Herbelin | 2015-11-18 |
* | Tests for syntax "Show id" and [id]:tac (shelved or not). | Hugo Herbelin | 2015-11-07 |
* | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | 2015-11-04 |
* | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau | 2015-10-29 |
* | Fix test suite after Matthieu's ed7af646f2e486b. | Maxime Dénès | 2015-10-28 |
* | Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" | Hugo Herbelin | 2015-10-28 |
* | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin | 2015-10-18 |
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin | 2015-10-11 |
* | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | 2015-10-08 |
* | Test for record syntax parsing. | Pierre-Marie Pédrot | 2015-10-07 |
* | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau | 2015-10-07 |
* | In pat/constr introduction patterns, fixing in a better way clearing problems | Hugo Herbelin | 2015-09-16 |
* | 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-09-08 |
* | 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-08-02 |
* | Extraction: fix primitive projection extraction. | Matthieu Sozeau | 2015-07-22 |
* | Univs: bug fix. | Matthieu Sozeau | 2015-07-07 |
* | Fix incompleteness of conversion used by evarconv | Matthieu Sozeau | 2015-06-28 |
* | Fixing incompatibility introduced with simpl in commit 364decf59c1 (or | Hugo Herbelin | 2015-06-23 |
* | Extraction: fix the detection of the "polyprop" situation | Pierre Letouzey | 2015-05-12 |
* | Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default). | Hugo Herbelin | 2015-05-09 |
* | Fixing treatment of recursive equations damaged by 857e82b2ca0d1. | Hugo Herbelin | 2015-05-06 |
* | Fixing test-suite. | Pierre-Marie Pédrot | 2015-04-01 |
* | 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-25 |
* | 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-24 |
* | Qed export -> Qed exporting | Enrico Tassi | 2015-03-22 |
* | Add some tests for tryif | Jason Gross | 2015-03-13 |
* | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | 2015-03-11 |
* | Add a test-suite file ensuring coinductives with primitive projections | Matthieu Sozeau | 2015-03-03 |
* | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin | 2015-02-27 |
* | 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-23 |
* | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | 2015-02-14 |
* | Adding a test-suite for tactic notation naming. | Pierre-Marie Pédrot | 2015-02-11 |
* | 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-17 |
* | Fix files in test-suite having to do with Require inside modules. | Maxime Dénès | 2015-01-12 |