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
*
doc Nstaz updated
pottier
2010-06-04
*
Backported r13068 to branch v8.3 (whd_betaiota on inferred return
herbelin
2010-06-04
*
A new command Compute foo, shortcut for Eval vm_compute in foo
letouzey
2010-06-04
*
Grobner.v removed
pottier
2010-06-04
*
"Improved" the form of the inferred type of "match" by
herbelin
2010-06-03
*
Added command "Locate Ltac qid".
herbelin
2010-06-03
*
Avoid computing tactic printing tree (std_ppcmds) when printing not needed in
herbelin
2010-06-03
*
plugins/xml: kill two warnings
letouzey
2010-06-03
*
Ocamlbuild: try to speed-up error detection in *.ml*, by byte-compiling first
letouzey
2010-06-03
*
Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4
letouzey
2010-06-03
*
Misc fixes related to new nsatz (and ocamlbuild)
letouzey
2010-06-03
*
Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)
glondu
2010-06-03
*
nsatz ajoute
pottier
2010-06-03
*
ajout oublie
pottier
2010-06-03
*
plugin groebner updated and renamed as nsatz; first version of the doc of nsa...
pottier
2010-06-03
*
Fix xml test in non-local mode
glondu
2010-06-02
*
Do not link system library into installed .cma
glondu
2010-06-02
*
Fix typos
glondu
2010-06-02
*
Fix test-suite cleaning
glondu
2010-06-02
*
Extraction: start of a support library
letouzey
2010-06-02
*
added -args option to coqide to pass options to coqtops
vgross
2010-06-01
*
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
*
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
[next]