aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2015-05-15Turning "Set Regular Subst Tactic" on by default (for 8.6).Hugo Herbelin
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-12Extraction: fix the detection of the "polyprop" situationPierre Letouzey
2015-05-09Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Hugo Herbelin
2015-05-06Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Hugo Herbelin
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-01Fixing test-suite.Pierre-Marie Pédrot
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-03-25Another example about the consequence of a wrong computation of theHugo Herbelin
2015-03-24Fixing computation of non-recursively uniform arguments in theHugo Herbelin
2015-03-24Fixing wrong rel_context in checking positivity condition.Hugo Herbelin
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-03-13Merge branch 'v8.5' into trunkArnaud Spiwack
2015-03-13Add some tests for tryifJason Gross
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-03Add a test-suite file ensuring coinductives with primitive projectionsMatthieu Sozeau
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Fixing first part of bug #3210 (inference of pattern-matching returnHugo Herbelin
2015-02-24Other tests for decl mode, coming from reference manual.Hugo Herbelin
2015-02-23Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Hugo Herbelin
2015-02-23Fixing occur-check which was too strong in unification.ml.Hugo Herbelin
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-11Adding a test-suite for tactic notation naming.Pierre-Marie Pédrot
2015-01-17Revert "Fix files in test-suite having to do with Require inside modules."Maxime Dénès
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-12Fix files in test-suite having to do with Require inside modules.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-01An optimization in the use of unification candidates so as to get theHugo Herbelin
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-10Fixing orientation of postponed subtyping problems.Hugo Herbelin
2014-12-07Improving evar restriction (this is a risky change, as I remember aHugo Herbelin
2014-12-04Take benefit of improved name preservation of evars in e2fa65fcc.Hugo Herbelin
2014-12-02When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifHugo Herbelin
2014-11-25Adapting to current semantics of "simpl non-evaluable-cst"Hugo Herbelin
2014-11-25Experimenting using unification when matching evar/meta free subtermsHugo Herbelin
2014-11-22Add test-suite file for dependent rewriting example by Vadim Zaliva andMatthieu Sozeau
2014-11-18Fixing a little bug with nested but convertible occurrences in "destruct at".Hugo Herbelin
2014-11-18Fixing detection of occurrences in the presence of nested subterms forHugo Herbelin
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-14Preserving the good effect of 014e5ac92a on not leaving dangling localHugo Herbelin
2014-11-13Removing yet another source of remaining local definitions.Hugo Herbelin
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:24:36 +0000