index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Correct wrong handling of evars in instance definitions that prevented
msozeau
2010-06-29
*
change the flag "internal" in declare/ind_tables from bool to
vsiles
2010-06-29
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Added regression tests for bugs + miscellaneous improvements
herbelin
2010-06-12
*
Applying François' patch fixing grammar of uniform inheritance condition mes...
herbelin
2010-06-12
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Automatic introduction of names given before ":" in Lemma's and
herbelin
2010-06-09
*
Fix treatment of {struct x} annotations in presence of generalized
msozeau
2010-06-08
*
fixing error message display.
vgross
2010-06-07
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Added command "Locate Ltac qid".
herbelin
2010-06-03
*
Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4
letouzey
2010-06-03
*
Cleanup: remove code specific for ocaml 3.06
letouzey
2010-06-01
*
restore handling of lexer errors
letouzey
2010-06-01
*
CoqIDE goes multiprocess
vgross
2010-05-31
*
More indirection.
vgross
2010-05-31
*
Introducing strong typing for IDE - toplevel IPC
vgross
2010-05-31
*
deporting Coq specific code from ide to toplevel.
vgross
2010-05-31
*
Modifying startup sequence
vgross
2010-05-31
*
New pass on inductive schemes
herbelin
2010-05-29
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Nicer representation of tokens, more independant of camlp*
letouzey
2010-05-19
*
static (and shared) camlp4use instead of per-file declaration
letouzey
2010-05-19
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Applicative commutative cuts in Fixpoint guard condition
pboutill
2010-05-18
*
- Fixing bug #2308 about Lemma ... with
vsiles
2010-05-04
*
Fail: a way to check that a command is refused without blocking a script
letouzey
2010-04-30
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Two forgotten $Id$ in last commit
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Fix bug #2245, incorrect handling of Context in sections inside module
msozeau
2010-04-27
*
Added a new exception for already declared Schemes,
vsiles
2010-04-27
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Applying François Garillot's patch (#2261 in bug tracker) for extended
herbelin
2010-04-22
*
missing space in error message
vsiles
2010-04-20
*
Granting wish #2249 (checking existing lemma name also when in a section).
herbelin
2010-04-09
*
Small improvements around coqdoc (including fix for bug #2288)
herbelin
2010-03-30
*
Improving error messages in the presence of utf-8 characters
herbelin
2010-03-30
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
*
Fixed bug #2260 (check of resolution of all evars in the declaration
herbelin
2010-03-24
*
Added automatic expansion on the left of recursive notations
herbelin
2010-03-23
*
Fix splitting evars tactics and stop dropping evar constraints when
msozeau
2010-03-15
*
No delta-reduction in libtypes anymore
puech
2010-03-11
*
Filter out "_subproof" objects from search results
puech
2010-03-11
*
Fix treatment of remaining unification constraints: raise a more
msozeau
2010-03-07
*
Fixes in rewrite and a Elimination/Case to Scheme:
msozeau
2010-03-06
*
Minor fixes.
msozeau
2010-03-05
[next]