aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Protection contre les renommages; redondancesGravatar herbelin2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5016 85f007b7-540e-0410-9357-904b9bb8a0f7
* commands renomme en queries, command goto a la place de forward to backwardt oGravatar marche2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplest Demo on modulesGravatar coq2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5014 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5013 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit precedentGravatar herbelin2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour des _eq en v8Gravatar herbelin2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5010 85f007b7-540e-0410-9357-904b9bb8a0f7
* Qualification des noms utilisateurs en cas de collision avec un nom nouveauGravatar herbelin2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5009 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monstrueuse inefficacite due a l'innocence du redacteur de la ligne vis a ↵Gravatar herbelin2003-11-27
| | | | | | vis de l'evaluation stricte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5008 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hint Destruct mal afficheGravatar barras2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5007 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation bug compilGravatar mohring2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5005 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5004 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5003 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ne_stringGravatar herbelin2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction de @; simplification traduction des identGravatar herbelin2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage de tactiques ltac coincidant avec certaines tactiques primitivesGravatar herbelin2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5000 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les notations videsGravatar herbelin2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de l'indicateur de date "@" par 'at'Gravatar herbelin2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export string_index_fromGravatar herbelin2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ↵Gravatar herbelin2003-11-26
| | | | | | Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4996 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* majGravatar filliatr2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Garder 'destruct using' a l'affichage ?Gravatar herbelin2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4992 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif lexer: ident peut commencer par _Gravatar barras2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Version preliminaire pour la V8Gravatar herbelin2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4990 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
* Traduction Print ProofGravatar herbelin2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4988 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
* textesGravatar marche2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4986 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4985 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4984 85f007b7-540e-0410-9357-904b9bb8a0f7
* aboutGravatar marche2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4983 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4982 85f007b7-540e-0410-9357-904b9bb8a0f7
* tentative de completion ESC-/ a la emacsGravatar letouzey2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4981 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
* Renoncement de la compatibilite des noms qualifies au profit de la ↵Gravatar herbelin2003-11-24
| | | | | | compatibilite des arguments implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4979 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4978 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4977 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4976 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJsGravatar herbelin2003-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des definitions locales dans les (co-)points-fixesGravatar herbelin2003-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4974 85f007b7-540e-0410-9357-904b9bb8a0f7
* CompatibiliteGravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traitement plus clair, notamment pour Locate, de quand quoter les ↵Gravatar herbelin2003-11-22
| | | | | | composantes de notations + contournement du fait que Lexer arrive apres Symbol git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug introduit avec le 'Simpl f'Gravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4970 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des niveaux videsGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4968 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout Pnat et Pcompare_antisymGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4967 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 13:30:45 +0000