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
...
*
Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 too
herbelin
2010-09-18
*
Fixing bugs #2347 (part 2) and #2388: error message printing was done
herbelin
2010-09-18
*
CoqIDE argv parsing delegated to coqtop
vgross
2010-09-14
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
* removed declare_constant and declare_internal_constant
vsiles
2010-09-02
*
v13392 port from v8.3 to trunk : correct message when defining inductive schemes
vsiles
2010-09-02
*
* By default, load proof terms.
regisgia
2010-08-31
*
* scripts/Coqc toplevel/Usage:
regisgia
2010-08-27
*
* toplevel/Coqtop: Reactivate -dont-load-proofs option.
regisgia
2010-08-27
*
* lib/Flags: Replace dont_load_proofs by load_proofs since not loading
regisgia
2010-08-27
*
Fix an error message ot having the ERror: prefix.
courtieu
2010-08-26
*
Rather quick hack to make basic unicode notations available by
herbelin
2010-07-29
*
Fix computation of fix annotation index: only consider assumptions and
msozeau
2010-07-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Some fine-tuning after removal of automatic imports of coercions in r13310
herbelin
2010-07-23
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Simplified the way internalization_data (i.e. bindings of bound vars
herbelin
2010-07-22
*
Constrintern: unified push_name_env and push_loc_name_env; made
herbelin
2010-07-22
*
Amelioration dans Function
jforest
2010-07-16
*
Fix goal display when backtracking
vgross
2010-07-05
*
Stronger checks on coqtop termination, warning when zombies.
vgross
2010-07-05
*
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
[prev]
[next]