aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Added the documentation on Functional Scheme (a command, I also putGravatar courtieu2003-06-21
| | | | | | | | some examples in RefMan-tacex.tex) and Functional Induction (a tactic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'in (Type of ...)'Gravatar herbelin2003-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8334 85f007b7-540e-0410-9357-904b9bb8a0f7
* DiversGravatar herbelin2003-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8333 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8332 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Simpl et ChangeGravatar herbelin2003-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajoute SubClassGravatar herbelin2003-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug de pr�c�denceGravatar herbelin2003-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pr�sentationGravatar herbelin2003-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8328 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8327 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8326 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la reference sur la doc Reals.psGravatar desmettr2003-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack faqGravatar herbelin2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8324 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Remark/FactGravatar herbelin2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8323 85f007b7-540e-0410-9357-904b9bb8a0f7
* BugGravatar herbelin2003-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8322 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug {Gravatar desmettr2003-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Release 7.4Gravatar desmettr2003-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8319 85f007b7-540e-0410-9357-904b9bb8a0f7
* version 7.4Gravatar filliatr2003-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8318 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ doc modulesGravatar coq2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Streicher (axiom K)Gravatar herbelin2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8316 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout {A New Paradox in Type Theory}Gravatar herbelin2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8314 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour RealsGravatar desmettr2003-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8313 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj du fichier treesort.ml inclus dans le chapitre extractionGravatar letouzey2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8312 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj extraction V7.4Gravatar letouzey2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement s�mantique Match termGravatar herbelin2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de 'Recursive' pour les tactiques r�cursivesGravatar herbelin2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8309 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ V7.4Gravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8308 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8307 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8306 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ LtacGravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8305 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc SearchAboutGravatar filliatr2003-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Definition -> Parameter dans module typesGravatar coq2002-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8303 85f007b7-540e-0410-9357-904b9bb8a0f7
* FAQGravatar herbelin2002-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stupid mistakeGravatar coq2002-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8301 85f007b7-540e-0410-9357-904b9bb8a0f7
* `\"' redevenu �chappement pour `"'Gravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8300 85f007b7-540e-0410-9357-904b9bb8a0f7
* typosGravatar letouzey2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation des notationsGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Doc module, premiere versionGravatar coq2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le fichier CHANGES au format html - version 7.3.1Gravatar herbelin2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8296 85f007b7-540e-0410-9357-904b9bb8a0f7
* avertissement Correctness plus d�velopp�Gravatar filliatr2002-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8295 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ eq_rect, False_rec, False_rectGravatar herbelin2002-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction typo d'un but TautoGravatar herbelin2002-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8293 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation variante Subst (sans argument)Gravatar filliatr2002-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8292 85f007b7-540e-0410-9357-904b9bb8a0f7
* SubstGravatar filliatr2002-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug Makefile docGravatar desmettr2002-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8290 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ syntaxe 'Hint Rewrite'Gravatar herbelin2002-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8289 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour de Sorting dans la biblio standardGravatar herbelin2002-08-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8288 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de remarques diverses sur les commandes vernaculairesGravatar herbelin2002-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Local Coercion -> Coercion Local (dans l'index)Gravatar filliatr2002-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8286 85f007b7-540e-0410-9357-904b9bb8a0f7