aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Using vernac parsing for FunctionGravatar jforest2010-06-08
* Extraction with implicits: perform the occur-check after optimisationsGravatar letouzey2010-06-08
* Fixed wrong spelling in a warning.Gravatar herbelin2010-06-08
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Typo in ExtrOcamlString: list char instead of char listGravatar letouzey2010-06-08
* Fix unfolding tactic for well-founded Programs.Gravatar msozeau2010-06-08
* Tentative fix for typeclass resolution raising Evd.define exceptions.Gravatar msozeau2010-06-08
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
* Fix commentGravatar glondu2010-06-07
* Document grammar.cma->unix.cma dependency in CHANGESGravatar glondu2010-06-07
* Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)Gravatar glondu2010-06-07
* fixing error message display.Gravatar vgross2010-06-07
* Backporting part of r12970 to trunk (deprecation of double induction).Gravatar herbelin2010-06-07
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Updated performance analysis fileGravatar herbelin2010-06-06
* Extraction: attempt to provide nice extraction of chars and strings for OcamlGravatar letouzey2010-06-04
* Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-...Gravatar letouzey2010-06-04
* Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intGravatar letouzey2010-06-04
* doc Nstaz updatedGravatar pottier2010-06-04
* Backported r13068 to branch v8.3 (whd_betaiota on inferred returnGravatar herbelin2010-06-04
* A new command Compute foo, shortcut for Eval vm_compute in fooGravatar letouzey2010-06-04
* Grobner.v removedGravatar pottier2010-06-04
* "Improved" the form of the inferred type of "match" byGravatar herbelin2010-06-03
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
* Avoid computing tactic printing tree (std_ppcmds) when printing not needed inGravatar herbelin2010-06-03
* plugins/xml: kill two warningsGravatar letouzey2010-06-03
* Ocamlbuild: try to speed-up error detection in *.ml*, by byte-compiling firstGravatar letouzey2010-06-03
* Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4Gravatar letouzey2010-06-03
* Misc fixes related to new nsatz (and ocamlbuild)Gravatar letouzey2010-06-03
* Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)Gravatar glondu2010-06-03
* nsatz ajouteGravatar pottier2010-06-03
* ajout oublieGravatar pottier2010-06-03
* plugin groebner updated and renamed as nsatz; first version of the doc of nsa...Gravatar pottier2010-06-03
* Fix xml test in non-local modeGravatar glondu2010-06-02
* Do not link system library into installed .cmaGravatar glondu2010-06-02
* Fix typosGravatar glondu2010-06-02
* Fix test-suite cleaningGravatar glondu2010-06-02
* Extraction: start of a support libraryGravatar letouzey2010-06-02
* added -args option to coqide to pass options to coqtopsGravatar vgross2010-06-01
* Cleanup: remove code specific for ocaml 3.06Gravatar letouzey2010-06-01
* restore handling of lexer errorsGravatar letouzey2010-06-01
* CoqIDE goes multiprocessGravatar vgross2010-05-31
* More indirection.Gravatar vgross2010-05-31
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
* Modifying startup sequenceGravatar vgross2010-05-31
* New pass on inductive schemesGravatar herbelin2010-05-29
* Typo in comment of proof.mlGravatar herbelin2010-05-29
* A little bit of cleanup, and some annotations.Gravatar fkirchne2010-05-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 02:58:13 +0000