index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
Commit message (
Expand
)
Author
Age
...
*
Synchronized names from the "as" clause with the skeleton of the
Hugo Herbelin
2014-06-30
*
Fix test-suite script for subst working with let-ins, the following proof was...
Matthieu Sozeau
2014-06-23
*
Changed syntax of explicit universes.
Matthieu Sozeau
2014-06-23
*
Fix canonical structure resolution in unification (bug found in Ssreflect).
Matthieu Sozeau
2014-06-08
*
- 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-06-04
*
More on injection over a projectable "existT". - Fixing syntax "injection ......
Hugo Herbelin
2014-05-31
*
Fixing introduction patterns * and ** when used in a branch so that they do n...
Hugo Herbelin
2014-05-31
*
- Fix in kernel conversion not folding the universe constraints
Matthieu Sozeau
2014-05-26
*
Simplification and improvement of "subst x" in such a way that it
Hugo Herbelin
2014-05-08
*
Comment in Funind.v test-suite file
Matthieu Sozeau
2014-05-06
*
- Fix arity handling in retyping (de Bruijn bug!)
Matthieu Sozeau
2014-05-06
*
Fix restrict_universe_context removing some universes that do appear in the t...
Matthieu Sozeau
2014-05-06
*
Fix declarations of monomorphic assumptions
Matthieu 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-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
test for apply + TC resolution
Enrico Tassi
2014-03-26
*
Pos.compare_cont takes the comparison as first argument
Pierre Boutillier
2014-02-28
*
Add a test suite file for Ltac's "+" tactical.
Arnaud Spiwack
2014-01-06
*
Remove duplicate test-suite file.
Arnaud Spiwack
2013-12-06
*
Fix the refine related test-suite files to account for the new refine.
Arnaud Spiwack
2013-12-06
*
Fixing some tests from the test-suite.
ppedrot
2013-09-03
*
* test-suite/success/Unicode_utf8:
regisgia
2013-09-02
*
More dynamic argument scopes
letouzey
2013-07-17
*
Continuing r16621 on injection intro-patterns:
herbelin
2013-07-10
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...
msozeau
2013-06-10
*
Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an
herbelin
2013-06-02
*
Fixing a regression in unification introduced in r16205 (error raised
herbelin
2013-05-14
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Declaration of multiple hypotheses or parameters now share typing
herbelin
2013-05-08
*
Share more information between constructors and arity of an inductive
herbelin
2013-05-08
*
Moved isolated test params_ind.v to Inductive.v.
herbelin
2013-05-08
*
Hack to solve a "Bad recursive type" anomaly.
herbelin
2013-05-05
*
Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.
herbelin
2013-03-21
*
Using hnf instead of "intro H" for forcing reduction to a product.
herbelin
2013-03-21
*
Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).
herbelin
2013-01-29
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Fix bug 2958: Inductive deep in in clause are impossible
pboutill
2013-01-21
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Taking into account the possibility of having a type of type which is
herbelin
2012-12-18
*
Fixed a little inefficiency of "set/destruct" over a pattern. Now
herbelin
2012-12-18
*
Backtrack on activating scopes with type casts (was r15978).
herbelin
2012-12-04
*
Evarconv: Fix #2936 + comments
pboutill
2012-11-28
*
Fixing test-suite: Scope.v
ppedrot
2012-11-21
*
Taking into account the type of a definition (if it exists), and the
herbelin
2012-11-17
*
test-suite: Local Tactic Notation is now legal since r15731
letouzey
2012-08-23
*
Unification in Evar_conv uses an abstract machine state
pboutill
2012-08-09
[prev]
[next]