aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2011-10-18Extraction.tex: typo in an Extract Inductive example (fix #2625)letouzey
2011-10-09mainbiblio.bib : get rid of merge marker from failed mergeletouzey
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
2011-10-07Remove 'status' of Program and explain the :> better, as well as referencing ...msozeau
2011-10-01Updating some links in the FAQherbelin
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-24Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev aboutherbelin
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
2011-09-17doc/refman/Extraction.tex: no need to actually build euclid.mlletouzey
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
2011-09-01Several bug reports came from confusions between generalize and set.pboutill
2011-09-01Bug 2583: Update of the syntax of terms in the reference manualpboutill
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-07-07coq_makefile documentation in Refman and -hpboutill
2011-07-04doc/stdlib: Update the list of ZArith filesletouzey
2011-06-29update of Micromega docfbesson
2011-06-16refman nsatzpottier
2011-05-06update of the file list in doc/stdlibletouzey
2011-04-28Adding "Tactic Notation" in doc index.herbelin
2011-04-15Documentation typo.gmelquio
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
2011-04-08@ in index of refman (last request of bug 2494)pboutill
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2011-03-17An option "Set Default Timeout n."letouzey
2011-03-05Restore documentation of library String which was removed in 2007 (r10049)herbelin
2011-02-10Remove obsolete TheoryListglondu
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-09Example of a simple ML tactic (Hello world).fkirchne
2010-12-06Numbers and bitwise functions.letouzey
2010-12-04Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).herbelin
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-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
2010-11-05Numbers: axiomatization, properties and implementations of gcdletouzey
2010-11-03Fix typo in "Hint Extern" docglondu
2010-11-02Document DOT output of universe graphglondu
2010-11-02Numbers : log2. Abstraction, properties and implementations.letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 11:25:53 +0000