index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Vernacentries: minor code cleanup
letouzey
2012-07-12
*
Bug 2838: ExplApp in mutual inductive parameters
pboutill
2012-07-12
*
Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfind
pboutill
2012-07-12
*
Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820
letouzey
2012-07-11
*
Also allow Reset in Load'ed files
letouzey
2012-07-11
*
Re-allow Reset in compiled files
letouzey
2012-07-11
*
Severe reorganisation of the code of tactics in Proofview.
aspiwack
2012-07-11
*
Fix regression introduced in r15418 that broke MathClasses. In program mode, ...
msozeau
2012-07-11
*
Fix typeclass error handling which was sometimes raising a Failure ("hd").
msozeau
2012-07-11
*
A friendlier printing of remaining goals when no goal is focused.
aspiwack
2012-07-11
*
Fixing Print Assumption display
ppedrot
2012-07-10
*
Restore test file induct.v where the "in |- *" is mandatory
letouzey
2012-07-10
*
isolate instances about Permutation and PermutationA which may slow rewrite
letouzey
2012-07-10
*
Better treatment of error messages in rewrite (avoid use of Errors.print).
msozeau
2012-07-10
*
Adapting the IDE interface with the focussed display.
ppedrot
2012-07-10
*
Small change in the printing of proofs for use by coqide.
aspiwack
2012-07-10
*
Fixes bug 2841 ([Focus 0] gives anomaly).
aspiwack
2012-07-10
*
Another correction to the dependent existential variable printing
aspiwack
2012-07-10
*
destruct: full compatibility with former _eqn syntax
letouzey
2012-07-09
*
Moved code out of ide_slave in a more appropriate place.
ppedrot
2012-07-09
*
The tactic remember now accepts a final eqn:H option (grant wish #2489)
letouzey
2012-07-09
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
*
Avoid a warning about unprintable new command Print Namespace
letouzey
2012-07-09
*
Fixed fake_ide test-suite.
ppedrot
2012-07-09
*
verbose compat notations : nicer option name
letouzey
2012-07-08
*
Restore an indentation of Show Script
letouzey
2012-07-07
*
Ring_polynom : a restricted simpl instead of a unfold;fold
letouzey
2012-07-07
*
Continuing r15459: it helps testing occur-check early in some
herbelin
2012-07-06
*
Minor fixes in the test-suite after my recent commits
letouzey
2012-07-06
*
Two adaptations after the changes of level of ->
letouzey
2012-07-06
*
BinPos/BinInt/BinNat : fix some argument scopes
letouzey
2012-07-06
*
Restore the compatibility notation Compare.not_eq_sym
letouzey
2012-07-06
*
Fix order of introduction of hints to preserve most-recent-first semantics.
msozeau
2012-07-06
*
A prototype implementation of a Print Namespace command.
aspiwack
2012-07-06
*
Fixes a bug in the parsing of the grammar entry dirpath which would,
aspiwack
2012-07-06
*
Practical fix for bug #1206 (anomaly raised in pretyping instead of
herbelin
2012-07-06
*
Fixes bug #2678
aspiwack
2012-07-06
*
Backtrack: add support for the "Proof c." syntax (fix #2832)
letouzey
2012-07-06
*
Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)
letouzey
2012-07-05
*
Legacy Ring and Legacy Field migrated to contribs
letouzey
2012-07-05
*
Quick update to CHANGES, mention especially the new parsing of ->
letouzey
2012-07-05
*
rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite
letouzey
2012-07-05
*
More cleanup in Ring_polynom and EnvRing
letouzey
2012-07-05
*
Some cleanup in recent proofs concerning pi
letouzey
2012-07-05
*
MSetRBT : elementary arith proofs instead of calls to lia
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
*
Open Scope can now also accepts delimiters (e.g. Z).
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
[next]