coq/doc/RecTutorial, branch master

Remove tutorials.

2018-05-10T17:23:49+00:00

[ltac] Deprecate nameless fix/cofix.

2018-04-13T10:13:48+00:00

LTAC's `fix` and `cofix` do require access to the proof object inside
the tactic monad when used without a name. This is a bit inconvenient
as we aim to make the handling of the proof object purely functional.

Alternatives have been discussed in #7196, and it seems that
deprecating the nameless forms may have the best cost/benefit ratio,
so opening this PR for discussion.

See also #6171.

Unbreak RecTutorial.v

2017-08-01T17:28:11+00:00

The RecTutorial.tex still contains similarly broken Coq code, it just
doesn't run it.

More consistent writing of de Bruijn.

2017-05-01T15:48:57+00:00

Switch the few remaining iso-latin-1 files to utf8

2014-12-09T13:27:21+00:00

"allows to", like "allowing to", is improper

2014-08-25T13:22:40+00:00

It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).

ZArith + other : favor the use of modern names instead of compat notations

2012-07-05T16:56:16+00:00

 - 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

mainbiblio.bib : get rid of merge marker from failed merge

2011-10-09T09:48:03+00:00

 Thanks to Tom Prince for spotting this

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14530 85f007b7-540e-0410-9357-904b9bb8a0f7

Delete trailing whitespaces in all .{v,ml} files

2009-09-17T15:58:14+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

Solves some warning and hides some not-bad ones in doc. It remains a

2009-01-29T17:05:59+00:00

few hevea warning (failure to put a vector on an expression in
Classes.tex, failure to support multirow in RecTutorial.tex).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11868 85f007b7-540e-0410-9357-904b9bb8a0f7