aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Expand)AuthorAge
...
* coq_makefile documentation in Refman and -hGravatar pboutill2011-07-07
* update of Micromega docGravatar fbesson2011-06-29
* refman nsatzGravatar pottier2011-06-16
* Adding "Tactic Notation" in doc index.Gravatar herbelin2011-04-28
* Documentation typo.Gravatar gmelquio2011-04-15
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
* remove old traces of SearchIsos (never ported to 7.x nor 8.x)Gravatar letouzey2011-04-12
* @ in index of refman (last request of bug 2494)Gravatar pboutill2011-04-08
* Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)Gravatar herbelin2011-04-06
* Add 'Existing Instances' declaration to declare multiple instances at once.Gravatar letouzey2011-04-06
* Update documentation concerning proofs loading (cf last commit)Gravatar letouzey2011-04-03
* Documentation of the timeout tactical (cf r13917)Gravatar letouzey2011-03-21
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
* Fix formatting issue in refmanGravatar glondu2011-01-12
* Remove references to -ide option of coqmktopGravatar glondu2011-01-11
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Precision in documentation of "decide equality"Gravatar glondu2010-12-24
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* More precise documentation for instantiateGravatar glondu2010-12-23
* Documentation for tactic constr_eqGravatar glondu2010-12-02
* Add tactic has_evar (#2433)Gravatar glondu2010-12-02
* Add tactic is_evar (Closes: #2433)Gravatar glondu2010-12-02
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
* Fix typo in "Hint Extern" docGravatar glondu2010-11-03
* Document DOT output of universe graphGravatar glondu2010-11-02
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
* More precise description of boolean ring in doc (see bug #2401)Gravatar glondu2010-10-11
* TeX input method is now supported upstreamGravatar vgross2010-10-07
* Remove Explain* vernacsGravatar glondu2010-10-06
* Remove VernacGoGravatar glondu2010-10-06
* (Hopefully) clearer explanation of Ltac's context patternsGravatar glondu2010-10-05
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Added a section in the documentation of Vernacular commands about Set/Unset/T...Gravatar aspiwack2010-09-23
* Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for png...Gravatar emakarov2010-09-06
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
* Minor fixes:Gravatar msozeau2010-07-27
* Documentation of Set Automatic Coercions Import.Gravatar herbelin2010-07-25
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Updating reference manual credits: gb is now nsatz.Gravatar herbelin2010-07-08
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
* modifs de nsatz suggerees par HugoGravatar pottier2010-06-25
* Documentation of clear dependent and revert dependentGravatar letouzey2010-06-18
* Update of Extraction documentationGravatar letouzey2010-06-14
* Extraction Implicit: documentationGravatar letouzey2010-06-14
* Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.Gravatar herbelin2010-06-11
* Fixed a very old (from V6.3) typo in headers.styGravatar herbelin2010-06-10
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Backporting part of r12970 to trunk (deprecation of double induction).Gravatar herbelin2010-06-07
* doc Nstaz updatedGravatar pottier2010-06-04
* A new command Compute foo, shortcut for Eval vm_compute in fooGravatar letouzey2010-06-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:43:38 +0000