aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* Update of credits filesGravatar herbelin2010-05-09
* Fix bug #2315 : printing of defined evars in Coqide.Gravatar aspiwack2010-05-07
* Deux commentaires retirés de ocamldoc.Gravatar aspiwack2010-05-07
* better detection of nested recursion in FunctionGravatar jforest2010-05-07
* Correction of a bug pointed by P. Casteran.Gravatar jforest2010-05-07
* Trying to find a problem pointed by P. CasteranGravatar jforest2010-05-07
* term matching in ltac was not coherent with match goal in presence of wildcar...Gravatar jforest2010-05-06
* Correction in Function documentationGravatar jforest2010-05-06
* Patch bug 2313.Gravatar soubiran2010-05-05
* Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofGravatar pboutill2010-05-05
* - Fixing bug #2308 about Lemma ... withGravatar vsiles2010-05-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-30 20:21:01 +0000