aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2014-09-08Fixing TestRefine test-suite file.Pierre-Marie Pédrot
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Fix primitive projections declarations for inductive records.Matthieu Sozeau
2014-09-04Add test-suite file for Case derivation on primitive records.Matthieu Sozeau
2014-09-03Yes another remaining clearing bug with 'apply in'.Hugo Herbelin
2014-09-02Adding a test-suite for second-order matching order and indexes.Pierre-Marie Pédrot
2014-09-02Another fix than 19a7a5789c to avoid descend_in_conjunction to useHugo Herbelin
2014-09-02An apply test.Hugo Herbelin
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-29Not using a "cut" in descend_in_conjunctions induced more success. WeHugo Herbelin
2014-08-28Fixing an unnatural selection of subterms larger than expected in theHugo Herbelin
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Fixing a bug introduced in the extension of 'apply in' + simplifying code.Hugo Herbelin
2014-08-18Fixing unification of subterms identified by patterns.Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-16Fixing too restrictive detection of resolution of evars in "apply in"Hugo Herbelin
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-07-11Fix Funind test-suite file after patch by Pierre.Matthieu Sozeau
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-30Synchronized names from the "as" clause with the skeleton of theHugo Herbelin
2014-06-23Fix test-suite script for subst working with let-ins, the following proof was...Matthieu Sozeau
2014-06-23Changed syntax of explicit universes.Matthieu Sozeau
2014-06-08Fix canonical structure resolution in unification (bug found in Ssreflect).Matthieu Sozeau
2014-06-04- Better parsing and printing of named universes: Type{ident} and foo@{(ident...Matthieu Sozeau
2014-06-04- Force every universe level to be >= Prop, so one cannot "go under" it anymore.Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-31More on injection over a projectable "existT". - Fixing syntax "injection ......Hugo Herbelin
2014-05-31Fixing introduction patterns * and ** when used in a branch so that they do n...Hugo Herbelin
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-08Simplification and improvement of "subst x" in such a way that itHugo Herbelin
2014-05-06Comment in Funind.v test-suite fileMatthieu Sozeau
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06Fix restrict_universe_context removing some universes that do appear in the t...Matthieu Sozeau
2014-05-06Fix declarations of monomorphic assumptionsMatthieu Sozeau
2014-05-06- Fix RecTutorial, and mutual induction schemes getting the wrong names.Matthieu Sozeau
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-26test for apply + TC resolutionEnrico Tassi
2014-02-28Pos.compare_cont takes the comparison as first argumentPierre Boutillier
2014-01-06Add a test suite file for Ltac's "+" tactical.Arnaud Spiwack
2013-12-06Remove duplicate test-suite file.Arnaud Spiwack
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-09-03Fixing some tests from the test-suite.ppedrot
2013-09-02* test-suite/success/Unicode_utf8:regisgia
2013-07-17More dynamic argument scopesletouzey
2013-07-10Continuing r16621 on injection intro-patterns:herbelin
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 03:59:13 +0000