aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Account for Stephane Glondu's remarks.Gravatar fkirchne2010-05-28
* Modify the test for csdp and associated message.Gravatar fkirchne2010-05-28
* Use existing functions to reimplement search_exe.Gravatar fkirchne2010-05-28
* ...Gravatar fkirchne2010-05-28
* Correction program_simplify. Devrait corriger certaines contribs.Gravatar aspiwack2010-05-28
* Generalized the formulation of classic_set in propositional contextsGravatar herbelin2010-05-28
* Minor fix in doc chapter on inference rules (added a missing space).Gravatar herbelin2010-05-28
* Documentation of pretype_id (minor commit).Gravatar herbelin2010-05-28
* Fixing Derive Inversion for new proof engineGravatar herbelin2010-05-26
* Added UIP_dec on suggestion of Eelis on #coq irc.Gravatar herbelin2010-05-22
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
* Added examples for checking that the guard condition excludes subtermsGravatar herbelin2010-05-20
* Fix bug 2307Gravatar pboutill2010-05-20
* fixed guard check with commutative cutsGravatar barras2010-05-20
* Mrec was not substituted correctlyGravatar barras2010-05-20
* Ocamlbuild: various fixGravatar letouzey2010-05-19
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayGravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
* Some ocamldoc comments + Fixing name of .coqrc.version file in refmanGravatar pboutill2010-05-18
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Missing warning flush in a lexer message + update of CHANGESGravatar herbelin2010-05-12
* Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.Gravatar herbelin2010-05-10
* Fix: Pfedit.get_current_goal_context when no goal is focused.Gravatar aspiwack2010-05-10
* Removed an evar_merge in clenv_fchain which not only is incorrect butGravatar herbelin2010-05-10
* Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)Gravatar herbelin2010-05-09
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 00:40:58 +0000