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
...
*
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
*
Correction of bug 2290 (removing stupid message)
jforest
2010-05-04
*
Correction of bug 2290
jforest
2010-05-04
*
ocamldoc related fixes
pboutill
2010-05-03
*
Re-enable validation in "make check", run it in parallel with test-suite
glondu
2010-05-03
*
Fix discrimination of sorts which doesn't play well with cumulativity
msozeau
2010-05-02
*
Extraction: fix type_expunge_from_sign broken in last commit
letouzey
2010-05-01
*
Extraction: an experimental command to get rid of some cst/constructor arguments
letouzey
2010-04-30
*
Fail: a way to check that a command is refused without blocking a script
letouzey
2010-04-30
*
"make source-doc" builds documentation of mli in html and pdf at
pboutill
2010-04-29
*
After the approval of Bruno, here the patch for the checker.
soubiran
2010-04-29
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
fixed bug #2224 (Error message in positivity check fixed)
vsiles
2010-04-29
[prev]
[next]