aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-06-08Fixed wrong spelling in a warning.herbelin
2010-06-08Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".herbelin
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-06-08Typo in ExtrOcamlString: list char instead of char listletouzey
2010-06-08Fix unfolding tactic for well-founded Programs.msozeau
2010-06-08Tentative fix for typeclass resolution raising Evd.define exceptions.msozeau
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-06-07Fix commentglondu
2010-06-07Document grammar.cma->unix.cma dependency in CHANGESglondu
2010-06-07Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)glondu
2010-06-07fixing error message display.vgross
2010-06-07Backporting part of r12970 to trunk (deprecation of double induction).herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-06-06Updated performance analysis fileherbelin
2010-06-04Extraction: attempt to provide nice extraction of chars and strings for Ocamlletouzey
2010-06-04Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-...letouzey
2010-06-04Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intletouzey
2010-06-04doc Nstaz updatedpottier
2010-06-04Backported r13068 to branch v8.3 (whd_betaiota on inferred returnherbelin
2010-06-04A new command Compute foo, shortcut for Eval vm_compute in fooletouzey
2010-06-04Grobner.v removedpottier
2010-06-03"Improved" the form of the inferred type of "match" byherbelin
2010-06-03Added command "Locate Ltac qid".herbelin
2010-06-03Avoid computing tactic printing tree (std_ppcmds) when printing not needed inherbelin
2010-06-03plugins/xml: kill two warningsletouzey
2010-06-03Ocamlbuild: try to speed-up error detection in *.ml*, by byte-compiling firstletouzey
2010-06-03Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4letouzey
2010-06-03Misc fixes related to new nsatz (and ocamlbuild)letouzey
2010-06-03Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)glondu
2010-06-03nsatz ajoutepottier
2010-06-03ajout oubliepottier
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-06-02Fix xml test in non-local modeglondu
2010-06-02Do not link system library into installed .cmaglondu
2010-06-02Fix typosglondu
2010-06-02Fix test-suite cleaningglondu
2010-06-02Extraction: start of a support libraryletouzey
2010-06-01added -args option to coqide to pass options to coqtopsvgross
2010-06-01Cleanup: remove code specific for ocaml 3.06letouzey
2010-06-01restore handling of lexer errorsletouzey
2010-05-31CoqIDE goes multiprocessvgross
2010-05-31More indirection.vgross
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
2010-05-31deporting Coq specific code from ide to toplevel.vgross
2010-05-31Modifying startup sequencevgross
2010-05-29New pass on inductive schemesherbelin
2010-05-29Typo in comment of proof.mlherbelin
2010-05-28A little bit of cleanup, and some annotations.fkirchne
2010-05-28Account for Stephane Glondu's remarks.fkirchne
2010-05-28Modify the test for csdp and associated message.fkirchne
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 18:43:16 +0000