aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
| | | | | | | | apparaît dans le but ou dans l'une des hypothèses (ferme les bugs #447, #883 et #1228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9201 85f007b7-540e-0410-9357-904b9bb8a0f7
* le parsing du LETIN ne suivait pas la DTD (bug #1237)Gravatar herbelin2006-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9200 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour sur la suppression du pf_nf (trop d'exemples utilisent avecGravatar herbelin2006-10-03
| | | | | | | | | | profit la simplification des arguments -- même si dans quelques cas trop de réduction obligent à revenir en arrière). Remplacement par un hack rapide (et non "scalable"). Suppression code mort oublié commit précédent sur equality.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ↵Gravatar herbelin2006-10-03
| | | | | | CSC) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9198 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveau ring/fieldGravatar barras2006-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9197 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug dans field_simplifyGravatar barras2006-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9196 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
| | | | | | | | | | | | | | | | | | Efficacité: - remplacement du typage par du re-typage léger - suppression d'un pf_nf suspect (cf bug #1173) [quid de la compatibilité ?] - remplacement des tests aveugles de projection impossible par un test qui vérifie au fur et à mesure que les filtrages sont autorisés Réorganisation: - factorisation des parties communes de injEq/discrEq/decompEq (à noter l'ordre inverse de génération des équations dans inj et decomp...) - uniformisation des noms "e" et "ee" utilisés dans la construction des combinateurs de discrimination Extension: - ajout d'une clause "as" à injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout allowed_sortsGravatar herbelin2006-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la comparaison (inutile) des paramètres globaux desGravatar herbelin2006-09-30
| | | | | | | | | | | | constructeurs dans la recherche des positions de divergence entre expressions construites (possible source d'inefficacité d'injection/discriminate dans le cas de paramètres globaux convertibles mais syntaxiquement distincts -- cf rapport de bug 1173, première suggestion, même si dans le cas soumis les paramètres sont syntaxiquement les mêmes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9193 85f007b7-540e-0410-9357-904b9bb8a0f7
* args implicites dans FieldGravatar barras2006-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new option -emacs-U changing emacs prompt delimiters byGravatar courtieu2006-09-29
| | | | | | | xml-like patterns (<prompt></prompt>). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9191 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reactivation des outils de developpement de JacekGravatar herbelin2006-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des warnings à la compilationGravatar notin2006-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9189 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 ↵Gravatar barras2006-09-29
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation de RealFieldGravatar barras2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des lignes vides dans l'affichage des scriptsGravatar notin2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9186 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 ↵Gravatar barras2006-09-28
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add dependent list combinators test.Gravatar msozeau2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile : COQLIB -> FULLCOQLIBGravatar corbinea2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9183 85f007b7-540e-0410-9357-904b9bb8a0f7
* Detection des paramettres pour les Functions bien fondeesGravatar jforest2006-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9182 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits pbs de dependancesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9181 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compilation newringGravatar notin2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9180 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit de field + renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed error mesg in decl modeGravatar corbinea2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrections mineuresGravatar notin2006-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Permet a un unfold de recevoir ses occurences a travers une variable Ltac.Gravatar letouzey2006-09-25
| | | | | | | | | | | | P.ex: Tactic Notation "test" integer(i) := unfold plus at i Ou meme: Tactic Notation "test" ne_integer_list(i) := unfold plus at i (voir commit 9159 d'Hugo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative d'amélioration du message d'erreur en cas de paramètre non laisséGravatar herbelin2006-09-24
| | | | | | | implicite dans une clause "in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug dans détection clause "in" mal formée quand le "in" estGravatar herbelin2006-09-24
| | | | | | | donné alors même qu'il n'est pas utile car ne lie aucun argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug de coercion de pattern introduit dans la 8.1betaGravatar herbelin2006-09-23
| | | | | | | | (les coercions ne marchaient plus quand le type du terme à filtrer était connu). Ajout d'un test pour ce bug et pour le bug #1168. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1168 (dans les coercions de pattern, c'est le nombreGravatar herbelin2006-09-23
| | | | | | | | de paramètres réels du constructeur qui compte et non le nombre total de paramètres de la coercion) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderGravatar herbelin2006-09-23
| | | | | | | leading to wrong/failing printing of notations such as "- 1" or "1 -"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wish #1187 granted (support for canonical structures that are recordsGravatar herbelin2006-09-23
| | | | | | | only up to some preliminary reductions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1229 (toplevel "unresolved evar" fled throughGravatar herbelin2006-09-23
| | | | | | | Declare Implicit Tactic support) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement surround dans util.ml et parenthésage des déclarationsGravatar herbelin2006-09-23
| | | | | | | | castées si aussi suivies de leur type (p.ex. dans les hypothèses de but), afin d'éviter des configurations non réinterprétables comme x:nat:nat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9164 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction filtrage des notations impliquant un "match" : la présenceGravatar herbelin2006-09-23
| | | | | | | | | | des localisations empêchait toute unification des pattern de filtrage de réussir. - Ajout au passage d'unification des pattern modulo alpha. - Exemples dans Notations.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection List.fold_left2 (cf bug #1224)Gravatar herbelin2006-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tout petit bug d'affichage dans constr_display (top_printers)Gravatar herbelin2006-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test Tactic NotationGravatar herbelin2006-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9160 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une valeur VList dans tacinterp pour permettre de cabler desGravatar herbelin2006-09-22
| | | | | | | | Tactic Notation acceptant des listes en entrée avec application à la définition de revert dans Tactics.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc du nouveau ringGravatar barras2006-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter ↵Gravatar herbelin2006-09-21
| | | | | | sans ouverture, comme c'est le cas pour les autres Hints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9157 85f007b7-540e-0410-9357-904b9bb8a0f7
* incomplete and temporary fix for PR#1222: revert accepts up to 10 argsGravatar letouzey2006-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9156 85f007b7-540e-0410-9357-904b9bb8a0f7
* better scope/require managment (patch by Russel O'Connor)Gravatar letouzey2006-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
* congruence doc updateGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Gestion des arguments implicites dans les Functions bien fondeesGravatar jforest2006-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9152 85f007b7-540e-0410-9357-904b9bb8a0f7
* added congruence improvementGravatar corbinea2006-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9151 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction of bug #1220Gravatar jforest2006-09-18
| | | | | | | adding a "using" optional argument to Function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1215Gravatar notin2006-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9149 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 04:01:15 +0000