aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-09-04test-suite uses coqtop instead of coqtop.bytepboutill
2012-09-04Erase %.vo dependency to the phony target statespboutill
2012-08-24In the output tests, ignore dynlink messagesletouzey
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
2012-08-24Use fully-qualified Coq.Init.Prelude when starting coqtopletouzey
2012-08-24Fix Extraction Implicit on axioms.aspiwack
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-24Better highlighting of strings in coqide.aspiwack
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
2012-08-24Modification of the unjustified tag.aspiwack
2012-08-24Correcting a comment in pattern-matching compilation.aspiwack
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
2012-08-23CHANGES: document the end of states/initial.coq and coqtop.optletouzey
2012-08-23Remove a script unused since 2006 (cf commit r8626)letouzey
2012-08-23myocamlbuild : fixes for new printing directory + sourceview for coqideletouzey
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
2012-08-23No need anymore to refer to COQLIB in ocamldebug-coqletouzey
2012-08-23Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"letouzey
2012-08-23Configure + Makefile : simplification when -localletouzey
2012-08-23configure: get rid of the -src option and of ${COQSRC}letouzey
2012-08-23configure: no more need for ocamlmktopletouzey
2012-08-23Extraction: document Separate Extraction and KeepSingletonletouzey
2012-08-23Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)letouzey
2012-08-23Port from 8.4 branch some build fixes concerning win32 :letouzey
2012-08-22Do not forget to build the unicode libraries, necessary to compile and launch...msozeau
2012-08-11Improving rendering of ldots in doc (partially done, there are tooherbelin
2012-08-11Some extra INCOMPATIBILITIES since 8.4.herbelin
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-11Some changes in CHANGES.herbelin
2012-08-11Improving rendering of ...-separated lists and sequences in referenceherbelin
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2012-08-10Bug 2861 : ocamlopt but no lablgtk2.cmxa problempboutill
2012-08-10Fixes bug #2857.aspiwack
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
2012-08-08Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.herbelin
2012-08-08Updating version numbers.herbelin
2012-08-08Documenting eta-conversion.herbelin
2012-08-08More standard layout for \lambda in chapter CIC.herbelin
2012-08-08Fixup for macOS 10.8 & Ocaml 4.0pboutill
2012-08-07Typo in r15654herbelin
2012-08-07Updating credits for final 8.4herbelin
2012-08-07Avoid Pp.std_ppcmds in Misctypes.sort_infoletouzey
2012-08-07configure: two minor fixes for win32letouzey
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
2012-08-06Coqdoc inlined verbatim_char in latexpboutill
2012-08-06Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) markup/typese...pboutill
2012-08-06Win32: some quote fixesletouzey