aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Collapse)AuthorAge
* just forgot something in previous commitGravatar corbinea2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4995 85f007b7-540e-0410-9357-904b9bb8a0f7
* removal of CC.v lemata in cc (deprecated)Gravatar corbinea2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation des politiques de nommage de NewDestruct sur arguments ↵Gravatar herbelin2003-11-25
| | | | | | recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
* CC: added injection theoryGravatar corbinea2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵Gravatar herbelin2003-11-24
| | | | | | passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code simplification in CCGravatar corbinea2003-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte renommagesGravatar herbelin2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4950 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction suite ajout nouvelles tactiquesGravatar clrenard2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Print Implicit avec depliage du typeGravatar herbelin2003-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ordre standard pour l'associativiteGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction chemin de ZGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4904 85f007b7-540e-0410-9357-904b9bb8a0f7
* moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵Gravatar barras2003-11-13
| | | | | | Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation et generalisation des clausesGravatar barras2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug TacIdGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration ZArithGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noms/énoncés plus canoniquesGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements de syntaxeGravatar barras2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
* les modifs depuis la 7.4Gravatar letouzey2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4858 85f007b7-540e-0410-9357-904b9bb8a0f7
* TODOGravatar letouzey2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Module M devient simplement Extraction MGravatar letouzey2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4856 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression SearchNamed finalement redondant avec SearchAboutGravatar herbelin2003-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4852 85f007b7-540e-0410-9357-904b9bb8a0f7
* le pb du <<.v vu comme module>> engendre maintenant une erreurGravatar letouzey2003-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4851 85f007b7-540e-0410-9357-904b9bb8a0f7
* message informant de l'ecriture d'un fichier extraitGravatar letouzey2003-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4850 85f007b7-540e-0410-9357-904b9bb8a0f7
* révision du traitement des axiomes non réalisésGravatar letouzey2003-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4849 85f007b7-540e-0410-9357-904b9bb8a0f7
* essai d'extraction sous un moduleGravatar letouzey2003-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4847 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation de (recursive) libraryGravatar letouzey2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4843 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction semantique des InHyp de clause en InHypValue si local defGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction semantique des InHyp de clause en InHypValue si local defGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Instantiate ... inGravatar corbinea2003-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout répertoire NArith pour l'arithmétique binaire sur les nombres ↵Gravatar herbelin2003-11-05
| | | | | | positifs et naturels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage canonique d'un lemme redondantGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déport des lemmes de Omega de ZArith vers OmegaLemmasGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage canonique d'un lemme redondantGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de zarithGravatar herbelin2003-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les buts sans inegaliteGravatar herbelin2003-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout CPatNotation, PrintVisibilityGravatar herbelin2003-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵Gravatar herbelin2003-11-01
| | | | | | entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redirected some of the verbose jprover output through the Pp module.Gravatar corbinea2003-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4746 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵Gravatar herbelin2003-10-30
| | | | | | associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
* traduction des noms de correctnessGravatar herbelin2003-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notations pour les expressions dans un anneauGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification preuveGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conjecture declare maintenant un axiome; reorganisation VernacDefinitionGravatar herbelin2003-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Jprover bugfix (hopefully !)Gravatar corbinea2003-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout NArithRingGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4703 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration de SearchNamed dans SearchAboutGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4698 85f007b7-540e-0410-9357-904b9bb8a0f7
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
| | | | | | | Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Construction des chemins de constantes plus robusteGravatar herbelin2003-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4690 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de l'utilisation de contradictionGravatar herbelin2003-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4674 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle syntaxe de ltacGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-18 02:16:14 +0000