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
*
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
*
Updating headers.
herbelin
2012-08-08
*
Improving management of notations with binders (see #2708 where a
herbelin
2012-07-21
*
Restore test file induct.v where the "in |- *" is mandatory
letouzey
2012-07-10
*
Legacy Ring and Legacy Field migrated to contribs
letouzey
2012-07-05
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Fixing bug #2809 (anomaly when printing a module with notations due to
herbelin
2012-06-20
*
Proof using: nested sections bugfix
gareuselesinge
2012-06-18
*
Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.
ppedrot
2012-06-12
*
Repair two tests
letouzey
2012-04-12
*
Relax uniform inheritance condition
gareuselesinge
2012-04-05
*
Unification: Added a heuristic to solve problems of the form
herbelin
2012-03-26
*
Fix the test-suite by removing any Reset in the scripts
letouzey
2012-03-23
*
evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures
gareuselesinge
2012-03-22
*
Fixing bug #2724 (using notations with binders in cases patterns
herbelin
2012-03-20
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
Fix bugs related to Program integration.
msozeau
2012-03-19
*
"Let in" in pattern hell, one more iteration
pboutill
2012-03-02
*
Use a heuristic to not simplify equality hypotheses remaining after dependent...
msozeau
2012-02-20
*
Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...
msozeau
2012-01-28
*
Backtracking on r14876 (fix for bug #2267): extra scopes might be
herbelin
2012-01-05
*
Type inference unification: fixed a 8.4 bug in the presence of unification
herbelin
2012-01-04
*
Fixing bug #2634 (unscoped notations were disturbing the
herbelin
2011-12-18
*
Fixed a Not_found bug when declaring in a section some implicit
herbelin
2011-12-18
*
Added ability to take the type of applied metas into account when
herbelin
2011-12-17
*
Proof using ...
gareuselesinge
2011-12-12
*
Fixing grammar resetting bug in the presence of levels initially empty
herbelin
2011-12-07
*
Fixing a bug of commit r13310 (activating coercions only when module
herbelin
2011-12-07
*
Discarding let-ins from the instances of the evars in the
herbelin
2011-12-04
*
Quick hack to avoid anomaly on using Program w/o having required JMeq.
herbelin
2011-11-30
*
Extraction: Richer patterns in matchs as proposed by P.N. Tollitte
letouzey
2011-11-28
*
Fixed a bug in postprocessing dependencies in pattern-matching compilation
herbelin
2011-11-26
*
Configurable simpl tactic
gareuselesinge
2011-11-21
*
Fixing postprocessing bugs in pattern-matching compilation.
herbelin
2011-11-21
*
Changed the way to detect if an "as" patterns is expanded or not. The
herbelin
2011-11-21
[next]