aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Bugfix: Fixing #3050Gravatar ppedrot2013-06-27
* 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
* Updating some output tests in test-suite:Gravatar herbelin2013-05-09
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Protection against "Bad recursive type" in w_unify0 (bug #3036).Gravatar herbelin2013-05-08
* 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
* Added a unit test for bug #2230.Gravatar ppedrot2013-04-27
* Finer fix for bug 3017, mark unresolvability only of goals that areGravatar msozeau2013-04-18
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
* Using Parameter instead of Variable in test-suite/outputGravatar herbelin2013-04-17
* Like in r16346, do not filter local definitions (here in theGravatar herbelin2013-04-17
* Added regression test for bug #3023 which was solved by Matthieu'sGravatar herbelin2013-04-16
* Equality: avoid some unprotected List.nth (fix #2837)Gravatar letouzey2013-04-10
* Enrich test-suite with a test for #3022.Gravatar ppedrot2013-04-08
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
* Enrich test-suite with a test for #2928Gravatar letouzey2013-03-25
* Enrich test-suite with a test for #2734Gravatar letouzey2013-03-25
* Add the test-case of bug 2750 in the test-suiteGravatar letouzey2013-03-25
* Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.Gravatar herbelin2013-03-21
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
* Firstorder: record with defined field aren't conjonctions (fix #2629)Gravatar letouzey2013-03-21
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
* Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)Gravatar letouzey2013-03-21
* Check a list length before doing a List.chop (fix #3000)Gravatar letouzey2013-03-20
* Fix for bug #3004 (thanks Hugo!)Gravatar letouzey2013-03-18
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* A slightly more efficient test of well-typedness of restriction ofGravatar herbelin2013-02-21
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
* Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenGravatar herbelin2013-02-05
* Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).Gravatar herbelin2013-01-29
* Added a file for testing regression of bug #2955 (anomaly in simpl inGravatar herbelin2013-01-29
* Fixing bug #2969 (admit failing after Grab Existential Variables dueGravatar herbelin2013-01-29
* Fixed bug #2966 (de Bruijn error in computation of heads for coercions).Gravatar herbelin2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Fixing one part of #2830 (anomaly "defined twice" due to nested calls toGravatar herbelin2013-01-28
* Fix bug 2958: Inductive deep in in clause are impossibleGravatar pboutill2013-01-21
* Last test-suite not in Symmetric Patterns syntaxGravatar pboutill2013-01-21
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Fixing parsing of specific primitive tokens used as notations for patternsGravatar herbelin2012-12-18
* Taking into account the possibility of having a type of type which isGravatar herbelin2012-12-18
* Fixed a little inefficiency of "set/destruct" over a pattern. NowGravatar herbelin2012-12-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:07:17 +0000