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
...
*
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
*
Typo in comment of proof.ml
herbelin
2010-05-29
*
A little bit of cleanup, and some annotations.
fkirchne
2010-05-28
*
Account for Stephane Glondu's remarks.
fkirchne
2010-05-28
*
Modify the test for csdp and associated message.
fkirchne
2010-05-28
*
Use existing functions to reimplement search_exe.
fkirchne
2010-05-28
*
...
fkirchne
2010-05-28
*
Correction program_simplify. Devrait corriger certaines contribs.
aspiwack
2010-05-28
*
Generalized the formulation of classic_set in propositional contexts
herbelin
2010-05-28
*
Minor fix in doc chapter on inference rules (added a missing space).
herbelin
2010-05-28
*
Documentation of pretype_id (minor commit).
herbelin
2010-05-28
*
Fixing Derive Inversion for new proof engine
herbelin
2010-05-26
*
Added UIP_dec on suggestion of Eelis on #coq irc.
herbelin
2010-05-22
*
Extract Inductive is now possible toward non-inductive types (e.g. nat => int)
letouzey
2010-05-21
*
Added examples for checking that the guard condition excludes subterms
herbelin
2010-05-20
*
Fix bug 2307
pboutill
2010-05-20
*
fixed guard check with commutative cuts
barras
2010-05-20
*
Mrec was not substituted correctly
barras
2010-05-20
*
Ocamlbuild: various fix
letouzey
2010-05-19
*
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
*
Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way
letouzey
2010-05-19
*
static (and shared) camlp4use instead of per-file declaration
letouzey
2010-05-19
*
Discontinue support for ocaml 3.09.*
letouzey
2010-05-19
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Some ocamldoc comments + Fixing name of .coqrc.version file in refman
pboutill
2010-05-18
*
Applicative commutative cuts in Fixpoint guard condition
pboutill
2010-05-18
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
Missing warning flush in a lexer message + update of CHANGES
herbelin
2010-05-12
*
Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.
herbelin
2010-05-10
*
Fix: Pfedit.get_current_goal_context when no goal is focused.
aspiwack
2010-05-10
*
Removed an evar_merge in clenv_fchain which not only is incorrect but
herbelin
2010-05-10
*
Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)
herbelin
2010-05-09
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Update of credits files
herbelin
2010-05-09
*
Fix bug #2315 : printing of defined evars in Coqide.
aspiwack
2010-05-07
*
Deux commentaires retirés de ocamldoc.
aspiwack
2010-05-07
*
better detection of nested recursion in Function
jforest
2010-05-07
*
Correction of a bug pointed by P. Casteran.
jforest
2010-05-07
*
Trying to find a problem pointed by P. Casteran
jforest
2010-05-07
*
term matching in ltac was not coherent with match goal in presence of wildcar...
jforest
2010-05-06
*
Correction in Function documentation
jforest
2010-05-06
*
Patch bug 2313.
soubiran
2010-05-05
*
Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof
pboutill
2010-05-05
*
- Fixing bug #2308 about Lemma ... with
vsiles
2010-05-04
[prev]
[next]