aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2007-01-17Correction adresse CoRN dans FAQ (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9492 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Correction adresse CoRN dans FAQ (cf #1317)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9491 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-23Doc for Combined Scheme.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9462 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Correction typo règle réduction du fix chapitre CCIherbelin
Maj mode emacs coqide dans faq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9412 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-01add a comment about Show Existentials and a question about case_eq jnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9408 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-11Typo + ajout Qcanon.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9366 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-02Add doc on obligation solving commands.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9332 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28MAJ nouvelles théoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9312 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Documentation de "Set Printing Universes", "Print Universes" (anciennementherbelin
"Dump Universes"), "Universe inconsistency", et description brève des univers algébriques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9306 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26added doc for declarative languagecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9286 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26MAJ crédits, fresh; documentation apply inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9283 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-16typo doc + bug legacy fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9243 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05revision de la semantique de rewrite ... in <clause>. details dans la docletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-04Ajout Stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9207 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-04Correction bug #1236notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9203 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-04Doc injection asherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9202 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28separation de RealFieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-22doc du nouveau ringbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9158 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20congruence doc updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9153 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-11Ajout eassumption indexherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9129 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-07Updating the doc about Function and cocourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9127 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Modification du manuel de référence: le flag evar pour cbv n'existe plus.notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9101 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28Ajout thèse Cornesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9089 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9080 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9079 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16MAJ Rectutorial (P. Castéran)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9068 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28MAJ de la biblio du manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9062 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-17MAJjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9051 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-12Documentation machine virtuelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9044 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11MAJ doc/refmannotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9040 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11Documentation de lazymatch et des extensions de idtac et failherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9038 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07Documentation Declare Implicit Tactic, Print Canonical Projections, ... + ↵herbelin
légère restructuration autour de Proof with et Hint Rewrite + maj crédits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9030 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07MAJ du manuel de référence (modules+fixpoints+pose proof)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9029 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-06Documentation Whelpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9028 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Ajout taclevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9019 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Documentation Print Ltac qualid; documentation du debugger de ltac.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9018 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Précisions sur l'Unicode reconnu; typo; ajout Example, Proposition, Corollary.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9013 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Mise à jour scopes prédéfinis et Tactic Notation pour tacticalsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9012 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Documentation 'external'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9011 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Doc Print Grammar patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9007 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Documentation or-patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9006 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Documentation or-patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9005 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Ajout cible refman-quick qui teste la compilation sans faire les index, toc ↵herbelin
et biblio git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9004 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Typo dans le manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9002 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Ajout espacement autour des symboles latex a l'attention de 'hevea -nosymb' ↵herbelin
+ modifs diverses de la présentation des règles d'inférence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9001 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04MAJ du manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 20:47:27 +0000