aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Extraction: fix primitive projection extraction.Gravatar Matthieu Sozeau2015-07-22
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* Fix incompleteness of conversion used by evarconvGravatar Matthieu Sozeau2015-06-28
* Fixing incompatibility introduced with simpl in commit 364decf59c1 (orGravatar Hugo Herbelin2015-06-23
* Extraction: fix the detection of the "polyprop" situationGravatar Pierre Letouzey2015-05-12
* Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Gravatar Hugo Herbelin2015-05-09
* Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Gravatar Hugo Herbelin2015-05-06
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-04-01
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Another example about the consequence of a wrong computation of theGravatar Hugo Herbelin2015-03-25
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* Add some tests for tryifGravatar Jason Gross2015-03-13
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Add a test-suite file ensuring coinductives with primitive projectionsGravatar Matthieu Sozeau2015-03-03
* Fixing first part of bug #3210 (inference of pattern-matching returnGravatar Hugo Herbelin2015-02-27
* Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Gravatar Hugo Herbelin2015-02-23
* Fixing occur-check which was too strong in unification.ml.Gravatar Hugo Herbelin2015-02-23
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Adding a test-suite for tactic notation naming.Gravatar Pierre-Marie Pédrot2015-02-11
* Revert "Fix files in test-suite having to do with Require inside modules."Gravatar Maxime Dénès2015-01-17
* Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
* Fix files in test-suite having to do with Require inside modules.Gravatar Maxime Dénès2015-01-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
* An optimization in the use of unification candidates so as to get theGravatar Hugo Herbelin2015-01-01
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
* Take benefit of improved name preservation of evars in e2fa65fcc.Gravatar Hugo Herbelin2014-12-04
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
* Adapting to current semantics of "simpl non-evaluable-cst"Gravatar Hugo Herbelin2014-11-25
* Experimenting using unification when matching evar/meta free subtermsGravatar Hugo Herbelin2014-11-25
* Add test-suite file for dependent rewriting example by Vadim Zaliva andGravatar Matthieu Sozeau2014-11-22
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Compatibility with 8.4 in the heuristic used to build the inductionGravatar Hugo Herbelin2014-11-08
* Restoring clear_flag (thanks a lot to jonikelee to notice it).Gravatar Hugo Herbelin2014-11-06
* Optimizing when to clear generalized hypotheses in destruct.Gravatar Hugo Herbelin2014-11-06
* Removing "destruct" test not yet working.Gravatar Hugo Herbelin2014-11-06
* Subtle swap of lines to preserve VarInstance src field before checkingGravatar Hugo Herbelin2014-11-03
* Fix to 844431761 on improving elimination with indices, getting rid ofGravatar Hugo Herbelin2014-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 09:40:00 +0000