aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-10-09Notations:herbelin
- prise en compte des variables liées non liées par la notation (bug #1186), - test pour affichage des notations aussi sur les sous-ensembles des lieurs multiples (cf notation "#" dans output/Notations.v), - extension, correction et uniformisation de quelques fonctions sur les constr_expr et cases_pattern (avec incidences sur rawterm.ml, parsing et contrib/interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Ajout combinateurs option_fold_left et name_fold_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06suite commit 9222 : rétablissement des tests autre que complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9224 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Remplacement des nf_evar (source de complexité polynomiale) par de laherbelin
réduction paresseuse. Accessoirement, suppression d'un test evar_defined inutile car sur résultat de whd_betadeltaiota qui contient la réduction evar de tête dans coercion.ml; code mort du commit précédent dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9223 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Ajout d'un répertoire de test de la complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9222 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Déplacement de on_judgment_type de Typeops vers Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9221 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Suppression d'une source de complexité polynomiale dans le pretypageherbelin
(remplacement de la normalisation complète des evars dans les termes par une normalisation par nécessité - dans les types, c'est en général des expressions plus petites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9220 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9219 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Annulation de l'essai de changement de sémantique du %scope (révision 9208).herbelin
Retour à une sémantique où les %scope s'appliquent à la sous-expression complète (trop de pbs: constantes polymorphes sans arguments scope, variables locales de type fonctionnel, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9218 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ↵notin
d'un constr c, on vérifie que c est clos dans l'environnement de m (#1183) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9217 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug #1242) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05revert, the previous commit was a mistakebertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9214 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05avertissement a propos du commit 9211 dans CHANGESletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9213 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05A version of natprering that should be more efficient and removal of a badbertot
comment in newring.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9212 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-05Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynombarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9210 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05Corrects the problem described in PR#1240:bertot
if natprering modified the goal, then ring_simplify only performed the operation as natprering. Now, goals that are solved by ring should also be solved by (ring_simplify; reflexivity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9209 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05Essai de changement de sémantique du %scope : herbelin
1- ne s'applique plus que sur la notation immédiate au lieu de s'appliquer récursivement pour toutes les notations de l'expression concernée; 2- désactive la pile de scope pour cette notation immédiate. Le point 2 est clairement préférable pour les notations de la forme 3%sc, où on ne veut pas que 3 soit interprété dans un autre scope que sc même si sc n'a pas de notations numériques. Le point 1 est plus discutable et risque aussi de poser des incompatibilité (mais le comportement récursif peut être rétabli en changeant la valeur de quelques booléens marqués "recursive" dans constrextern.ml, constrintern.ml, et notation.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9208 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-04inefficacite de field_simplify_eqbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9206 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-04Correction bug #1211notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9205 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-04Correction bug #1204 + maj CHANGESnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9204 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-10-03Changement de comportement du [rewrite ... in H]: Coq échoue si Hnotin
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
2006-10-03le parsing du LETIN ne suivait pas la DTD (bug #1237)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9200 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-03Retour sur la suppression du pf_nf (trop d'exemples utilisent avecherbelin
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
2006-10-03Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ↵herbelin
CSC) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9198 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-02nouveau ring/fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9197 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-02bug dans field_simplifybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9196 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-01Une passe sur l'injection et la discrimination...herbelin
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
2006-10-01Ajout allowed_sortsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9194 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-30Suppression de la comparaison (inutile) des paramètres globaux desherbelin
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
2006-09-29args implicites dans Fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9192 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-29Added a new option -emacs-U changing emacs prompt delimiters bycourtieu
xml-like patterns (<prompt></prompt>). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9191 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-29Reactivation des outils de developpement de Jacekherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9190 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-29Suppression des warnings à la compilationnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9189 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-29git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 ↵barras
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-28Suppression des lignes vides dans l'affichage des scriptsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9186 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 ↵barras
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28Add dependent list combinators test.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9184 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28Makefile : COQLIB -> FULLCOQLIBcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9183 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-27Detection des paramettres pour les Functions bien fondeesjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9182 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26petits pbs de dependancesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9181 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26Compilation newringnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9180 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26commit de field + renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26fixed error mesg in decl modecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9177 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-25Corrections mineuresnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9176 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 00:37:37 +0000