aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Fix Funind test-suite file after patch by Pierre.Gravatar Matthieu Sozeau2014-07-11
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Synchronized names from the "as" clause with the skeleton of theGravatar Hugo Herbelin2014-06-30
* Fix test-suite script for subst working with let-ins, the following proof was...Gravatar Matthieu Sozeau2014-06-23
* Changed syntax of explicit universes.Gravatar Matthieu Sozeau2014-06-23
* Fix canonical structure resolution in unification (bug found in Ssreflect).Gravatar Matthieu Sozeau2014-06-08
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Simplification and improvement of "subst x" in such a way that itGravatar Hugo Herbelin2014-05-08
* Comment in Funind.v test-suite fileGravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context removing some universes that do appear in the t...Gravatar Matthieu Sozeau2014-05-06
* Fix declarations of monomorphic assumptionsGravatar Matthieu Sozeau2014-05-06
* - Fix RecTutorial, and mutual induction schemes getting the wrong names.Gravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* test for apply + TC resolutionGravatar Enrico Tassi2014-03-26
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
* Add a test suite file for Ltac's "+" tactical.Gravatar Arnaud Spiwack2014-01-06
* Remove duplicate test-suite file.Gravatar Arnaud Spiwack2013-12-06
* Fix the refine related test-suite files to account for the new refine.Gravatar Arnaud Spiwack2013-12-06
* Fixing some tests from the test-suite.Gravatar ppedrot2013-09-03
* * test-suite/success/Unicode_utf8:Gravatar regisgia2013-09-02
* More dynamic argument scopesGravatar letouzey2013-07-17
* Continuing r16621 on injection intro-patterns:Gravatar herbelin2013-07-10
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...Gravatar msozeau2013-06-10
* Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anGravatar herbelin2013-06-02
* Fixing a regression in unification introduced in r16205 (error raisedGravatar herbelin2013-05-14
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Declaration of multiple hypotheses or parameters now share typingGravatar herbelin2013-05-08
* Share more information between constructors and arity of an inductiveGravatar herbelin2013-05-08
* Moved isolated test params_ind.v to Inductive.v.Gravatar herbelin2013-05-08
* Hack to solve a "Bad recursive type" anomaly.Gravatar herbelin2013-05-05
* Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.Gravatar herbelin2013-03-21
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
* Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).Gravatar herbelin2013-01-29
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 23:37:18 +0000