aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2010-05-28Use existing functions to reimplement search_exe.fkirchne
2010-05-28...fkirchne
2010-05-28Correction program_simplify. Devrait corriger certaines contribs.aspiwack
2010-05-28Generalized the formulation of classic_set in propositional contextsherbelin
2010-05-28Minor fix in doc chapter on inference rules (added a missing space).herbelin
2010-05-28Documentation of pretype_id (minor commit).herbelin
2010-05-26Fixing Derive Inversion for new proof engineherbelin
2010-05-22Added UIP_dec on suggestion of Eelis on #coq irc.herbelin
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
2010-05-20Added examples for checking that the guard condition excludes subtermsherbelin
2010-05-20Fix bug 2307pboutill
2010-05-20fixed guard check with commutative cutsbarras
2010-05-20Mrec was not substituted correctlybarras
2010-05-19Ocamlbuild: various fixletouzey
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-05-19Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayletouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Discontinue support for ocaml 3.09.*letouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 08:59:07 +0000