aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2011-01-12Fix formatting issue in refmanglondu
2011-01-11Remove references to -ide option of coqmktopglondu
2011-01-11Add "Print Sorted Universes"glondu
2010-12-24Precision in documentation of "decide equality"glondu
2010-12-23Remove the two-argument variant of "decide equality"glondu
2010-12-23More precise documentation for instantiateglondu
2010-12-02Documentation for tactic constr_eqglondu
2010-12-02Add tactic has_evar (#2433)glondu
2010-12-02Add tactic is_evar (Closes: #2433)glondu
2010-11-19SearchAbout: who has never been annoyed by the [ ] syntax ?letouzey
2010-11-03Fix typo in "Hint Extern" docglondu
2010-11-02Document DOT output of universe graphglondu
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
2010-10-11More precise description of boolean ring in doc (see bug #2401)glondu
2010-10-07TeX input method is now supported upstreamvgross
2010-10-06Remove Explain* vernacsglondu
2010-10-06Remove VernacGoglondu
2010-10-05(Hopefully) clearer explanation of Ltac's context patternsglondu
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-23Added a section in the documentation of Vernacular commands about Set/Unset/T...aspiwack
2010-09-06Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for png...emakarov
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-27Minor fixes:msozeau
2010-07-25Documentation of Set Automatic Coercions Import.herbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-08Updating reference manual credits: gb is now nsatz.herbelin
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
2010-06-25modifs de nsatz suggerees par Hugopottier
2010-06-18Documentation of clear dependent and revert dependentletouzey
2010-06-14Update of Extraction documentationletouzey
2010-06-14Extraction Implicit: documentationletouzey
2010-06-11Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.herbelin
2010-06-10Fixed a very old (from V6.3) typo in headers.styherbelin
2010-06-08Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".herbelin
2010-06-07Backporting part of r12970 to trunk (deprecation of double induction).herbelin
2010-06-04doc Nstaz updatedpottier
2010-06-04A new command Compute foo, shortcut for Eval vm_compute in fooletouzey
2010-06-03ajout oubliepottier
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-05-28Minor fix in doc chapter on inference rules (added a missing space).herbelin
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-05-18Some ocamldoc comments + Fixing name of .coqrc.version file in refmanpboutill
2010-05-09Update of credits filesherbelin
2010-05-06Correction in Function documentationjforest
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-27 small detail about Scheme Equality vsiles
2010-04-22Applying François Garillot's patch (#2261 in bug tracker) for extendedherbelin
2010-04-09Documenting the use of ##, %%, $$ in coqdoc.herbelin
2010-04-09Applied Cédric Auger's patch to fix use of "#&xxx;" in html printingherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 19:26:39 +0000