aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2012-07-25documentation of bullets (forward port from v8.4).courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15654 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-20Vector equalities first stuffpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10isolate instances about Permutation and PermutationA which may slow rewriteletouzey
After discovering a rewrite in Ergo that takes a loooong time due to a bad interaction with the instances of Permutation and PermutationA : - PermutationA is now in a separate file SetoidPermutation - File Permutation.v isn't Require'd by SetoidList anymore nor MergeSort.v, just the definitions in Sorted.v - Attempt to put a priority on these instances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
The ugly syntax "destruct x as [ ]_eqn:H" is replaced by: destruct x eqn:H destruct x as [ ] eqn:H Some with induction. Of course, the pattern behind "as" is arbitrary. For an anonymous version, H could be replaced by ?. The old syntax with "_eqn" still works for the moment, by triggers a warning. For making this new syntax work, we had to change the seldom-used "induction x y z using foo" into "induction x, y, z using foo". Now, only one "using" can be used per command instead of one per comma-separated group earlier, but I doubt this will bother anyone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12make sure that documentation compilation works after adding files forbertot
arc tangent and computations of PI approximations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15436 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-25Fixed #2789.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15360 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-10Addedum to documentation of bullets: I now use the dedicated coq_exampleaspiwack
environment to display the example. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-10Documentation for Unfocused, braces and bullets.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15293 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Rephrasing section on Sorts in CIC chapter, accordingly to discussionsherbelin
with Assia and Guillaume. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15284 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Ref. man., ch. CIC: clarifying the redundancy coming from having bothherbelin
Prop <= Type(i) and the conjunction of Prop <= Set and Set <= Type(i). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15283 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-03Fixup r15251 second timepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15275 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Removed the quasi-useless gtk2rc file and the documentation that went with ↵ppedrot
it. Now CoqIDE is not anymore totally irrespectful of the local configuration of themes, in particular w.r.t. to menu fonts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15251 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
Initial contribution by Andrew Appel, many ulterior modifications by myself. Interest: red-black trees maintain logarithmic depths as AVL, but they do not rely on integer height annotations as AVL, allowing interesting performance when computing in Coq or after standard extraction. More on this topic in the article by A. Appel. The common parts of MSetAVL and MSetRBT are shared in a new file MSetGenTree which include the definition of tree and functions such as mem fold elements compare subset. Note that the height of AVL trees is now the first arg of the Node constructor instead of the last one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-13Uniformisation in the documentation: remove the use of 'coinductive' inaspiwack
favour of 'co-inductive'. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15162 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-13Documentation of records defined with the keywords Inductive andaspiwack
CoInductive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15161 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-13Restores pdf bookmarks in the reference manual.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15160 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12lib directory is cut in 2 cma.pboutill
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
longer be bound to Funclass or Sortclass (this does not seem to be useful). [An exception is when using modules, if a constant foo is expanded into a type, a "Bind Scope sc with foo" starts binding Sortclass]. Also reworked reference manual for Arguments Scopes and Bind Scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15098 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Documentation of last commit concerning Backtrackingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15086 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
There're not compatible with the current Backtrack mecanism used both by ProofGeneral and CoqIDE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-19RefMan: Environment variables description updatepboutill
There is no mention in the refman of relative search of the lib from the binaries directory and of the use of _CoqProject by CoqIdE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15052 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29RefMan update about match syntax.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-20- changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵notin
available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-18Document the [unify] tactic.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-07Documentation for Grab Existential Variables.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-01Corrected a careless cut-and-paste in Gallina description which dated back ↵ppedrot
to 2003. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-01Improved synchronisation of stdlib index page with current library state.herbelin
- Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31index-list.html.template: add missing filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-21Coqtop and coqc: cleaning description of options in RefMan and manpages.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Added documentation for "r foo" in Ltac debugger.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14931 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
committed "assert" in commit r14928. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-19Added the btauto tactic to the documentation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14921 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-26Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14864 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-25Version number, copyright, credits: missing updates.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-23Credits for 8.4: More exhaustive list of external contributors.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-12Proof using ...gareuselesinge
New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Html page titlespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14774 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Documentation of Arguments + implicitsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14769 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Documentation for Arguments + notation scopesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14768 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Documentation for Arguments + simplgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14767 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-04Fixing bugs in doc about when "with" is needed or not to give bindingsherbelin
to tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14761 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Documentation of appcontextletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14744 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 15:45:50 +0000