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
*
correct some ends of .mllib files (avoid a broken tolink.ml)
letouzey
2012-08-24
*
Use fully-qualified Coq.Init.Prelude when starting coqtop
letouzey
2012-08-24
*
Fix Extraction Implicit on axioms.
aspiwack
2012-08-24
*
Experimental support for a comment in the files' preamble in extraction.
aspiwack
2012-08-24
*
Add option Set/Unset Extraction Conservative Types.
aspiwack
2012-08-24
*
Better highlighting of strings in coqide.
aspiwack
2012-08-24
*
Assumption commands are now displayed as unsafe in Coqide.
aspiwack
2012-08-24
*
Modification of the unjustified tag.
aspiwack
2012-08-24
*
Correcting a comment in pattern-matching compilation.
aspiwack
2012-08-24
*
test-suite: Local Tactic Notation is now legal since r15731
letouzey
2012-08-23
*
CHANGES: document the end of states/initial.coq and coqtop.opt
letouzey
2012-08-23
*
Remove a script unused since 2006 (cf commit r8626)
letouzey
2012-08-23
*
myocamlbuild : fixes for new printing directory + sourceview for coqide
letouzey
2012-08-23
*
No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey
2012-08-23
*
No more coqtop.opt, produce directly a coqtop binary
letouzey
2012-08-23
*
No need anymore to refer to COQLIB in ocamldebug-coq
letouzey
2012-08-23
*
Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"
letouzey
2012-08-23
*
Configure + Makefile : simplification when -local
letouzey
2012-08-23
*
configure: get rid of the -src option and of ${COQSRC}
letouzey
2012-08-23
*
configure: no more need for ocamlmktop
letouzey
2012-08-23
*
Extraction: document Separate Extraction and KeepSingleton
letouzey
2012-08-23
*
Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)
letouzey
2012-08-23
*
Port from 8.4 branch some build fixes concerning win32 :
letouzey
2012-08-23
*
Do not forget to build the unicode libraries, necessary to compile and launch...
msozeau
2012-08-22
*
Improving rendering of ldots in doc (partially done, there are too
herbelin
2012-08-11
*
Some extra INCOMPATIBILITIES since 8.4.
herbelin
2012-08-11
*
Added support for option Local (at module level) in Tactic Notation.
herbelin
2012-08-11
*
Some changes in CHANGES.
herbelin
2012-08-11
*
Improving rendering of ...-separated lists and sequences in reference
herbelin
2012-08-11
*
fast bitwise operations (lor,land,lxor) on int31 and BigN
letouzey
2012-08-11
*
Bug 2861 : ocamlopt but no lablgtk2.cmxa problem
pboutill
2012-08-10
*
Fixes bug #2857.
aspiwack
2012-08-10
*
Unification in Evar_conv uses an abstract machine state
pboutill
2012-08-09
*
Updating headers.
herbelin
2012-08-08
*
Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.
herbelin
2012-08-08
*
Updating version numbers.
herbelin
2012-08-08
*
Documenting eta-conversion.
herbelin
2012-08-08
*
More standard layout for \lambda in chapter CIC.
herbelin
2012-08-08
*
Fixup for macOS 10.8 & Ocaml 4.0
pboutill
2012-08-08
*
Typo in r15654
herbelin
2012-08-07
*
Updating credits for final 8.4
herbelin
2012-08-07
*
Avoid Pp.std_ppcmds in Misctypes.sort_info
letouzey
2012-08-07
*
configure: two minor fixes for win32
letouzey
2012-08-07
*
Vecnacentries.dump_global silently ignores exceptions
pboutill
2012-08-06
*
Coqdoc inlined verbatim_char in latex
pboutill
2012-08-06
*
Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) markup/typese...
pboutill
2012-08-06
*
Win32: some quote fixes
letouzey
2012-08-06
*
MSetRBT: a tail-recursive plength
letouzey
2012-08-06
*
Try to make the use of Unix.lockf in micromega compatible with Win32
letouzey
2012-08-06
*
Dump references in Extraction
pboutill
2012-08-05
[next]