aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Collapse)Author
2011-10-18Extraction.tex: typo in an Extract Inductive example (fix #2625)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14574 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14524 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Remove 'status' of Program and explain the :> better, as well as referencing ↵msozeau
it properly in the syntax of terms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14522 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
Tactics set/remember and destruct/induction take benefit of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14490 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-17doc/refman/Extraction.tex: no need to actually build euclid.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14478 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
Even if they are no-ops now, the commands Set/Unset Undo themselves are kept for compatibility, in particular to avoid error messages or warnings during the initialization of ProofGeneral. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14451 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
+ s/cbv/lazy of bug 2542 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14446 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Several bug reports came from confusions between generalize and set.pboutill
Maybe, people will read the two sections of the ref-man at the same time if they are one after the other... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14426 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Bug 2583: Update of the syntax of terms in the reference manualpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14425 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
when printing. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile documentation in Refman and -hpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14270 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-29update of Micromega docfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-16refman nsatzpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14211 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Adding "Tactic Notation" in doc index.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14076 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-15Documentation typo.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14008 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14Add directories in COQPATH to search path.herbelin
This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08@ in index of refman (last request of bug 2494)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13977 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
This is useful, for example, in declaring the projection of the dependent record bundled form of an unbundled typeclass. Patch submitted by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13954 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17An option "Set Default Timeout n."letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-12Fix formatting issue in refmanglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13791 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Remove references to -ide option of coqmktopglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Add "Print Sorted Universes"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24Precision in documentation of "decide equality"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13752 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Remove the two-argument variant of "decide equality"glondu
This variant was ignoring its second argument, and didn't exactly respect its documented specification. This is fixed by removing the variant altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13746 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23More precise documentation for instantiateglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13741 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Documentation for tactic constr_eqglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13665 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Add tactic has_evar (#2433)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13664 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Add tactic is_evar (Closes: #2433)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13663 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-19SearchAbout: who has never been annoyed by the [ ] syntax ?letouzey
Well, hopefully, that belongs to the past: you should now be able to do the very same queries as before, without typing the [ ]. For instance: SearchAbout plus mult. This removal of [ ] is optional, the old syntax is still legal: - for compatibility reasons - for square bracket lovers - for those that have "inside" or "outside" as legal identifier in their development and want to search about them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13654 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-03Fix typo in "Hint Extern" docglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13618 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Document DOT output of universe graphglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13612 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
Beware! after this, a ./configure must be done. It might also be a good idea to chase any phantom .vo remaining after a make clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-11More precise description of boolean ring in doc (see bug #2401)glondu
Also remove misleading example about classical propositional logic in "What does this tactic do?" section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13523 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-07TeX input method is now supported upstreamvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-06Remove Explain* vernacsglondu
Basically untouched since 1999. Same fate as VernacGo (r13506). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13510 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-06Remove VernacGoglondu
I agree with Arnaud on this one... Archeology: I could trace it back to r133 (in 1999!), and it was adapted to many big changes, including change of parsing (r2722, in 2002). Maybe it was used by Centaur or something similar once... The only relevant occurrences of "Go" in SVN history (since initial commit in 1999) is that it "semble peu robuste aux erreurs", without a clear specification of what it is supposed to do... Looks like an interesting feature, though, but needs complete rethinking (and documentation) with the new engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13506 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-05(Hopefully) clearer explanation of Ltac's context patternsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13503 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-03Added multiple implicit arguments rules per name.herbelin
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-23Added a section in the documentation of Vernacular commands about ↵aspiwack
Set/Unset/Test. It allowed to document the behaviour of Local and Global on Set and Unset. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13456 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-06Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for ↵emakarov
pngtopnm and pnmtops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27Minor fixes:msozeau
- Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-25Documentation of Set Automatic Coercions Import.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Extension of the recursive notations mechanismherbelin
- Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 14:01:56 +0000