aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2002-05-14Utilisation d'une construction spéciale SECVAR pour gérer laherbelin
globalisation des variables de section (en espérant plus de robustesse vis à vis des bugs récurrents de Infix pour les variables avec implicites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2684 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-03Simplification du filtrage si la premiere ligne de motifs est inevitable + ↵herbelin
autres bugs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2665 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-11Deuxième passe sur la localisation des messages d'erreurs sur les evars non ↵herbelin
définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2633 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08export de la fonction Reductionops.find_conclusion pour l'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2617 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-28petite erreur dans le typage des let-inbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2573 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-26Prise en compte des dependances dans la tactique Casemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21Décomposition de l'application n-aire en application binaire pour que ↵herbelin
Pattern réussisse sur des motifs partiellement appliqués git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2560 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-01Nouveau comportement: Delta ne s'applique pas aux variables liées par un letherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2506 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19typage du produit: type_judgment appele avec contexte incorrectbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2488 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19meilleur message d'erreur lorsqu'on type une evar qui n'existe pasbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2487 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19Le type des evars transformees en meta n'etait pas normalise, et des Evarsbarras
definies y apparaissait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2486 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-18bug #134: on appelait solve_simple_eqn avec une evar qui etait resoluebarras
par comparaison de ses arguments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2483 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12petite modif pour ne pas expanser trop de let pendant l'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2471 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-11substitution et pattern modulo letbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07petit nettoyage de kernel/inductivebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-04exceptionmal ratrappeebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2451 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31changement generation de schema d'elimination, False_rec est primitif, ↵mohring
Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25Correction bug 'Check [b]if b then O else O'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2435 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-24code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2429 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-24Réparation bug 'known_dependent'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2426 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-21warning en mode verbeux seulementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2422 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Le chargement des coercions est nécessaire même si le module n'est pas ouvertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2409 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-17Amélioration affichage échec lookup_eliminatorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2403 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-16Correction d'un problème avec les motifs anonymes dépendant dans des ↵herbelin
arguments implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2399 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-15Correction de de Bruijn incorrect pour le cas de dépendances vers l'avantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2396 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-20Non dépliage des Fix non réductibles dans Hnfherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2354 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Insertion unification non seulement en tête mais à l'intérieur des motifs ↵herbelin
(permet p.ex. de traiter le motif (Some O)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2322 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Grossière erreur de typageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2305 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Nettoyage exceptions liées au vieux Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Nettoyage exceptions liées au vieux Case; réparation du try with UserError ↵herbelin
mal nommé dans findtype git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2303 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Contournement du problème des evars de type, typées par défaut dans Type ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2295 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Contournement du problème des evars de type, typées par défaut dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2293 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11Mise en place de coercion dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2285 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-22La mise en forme normale du prédicat d'élimination était un peu trop ↵herbelin
violente pour la compatibilité de la synthèse des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2241 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Quelques autres petits problèmes résolus...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2239 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Simplification de la propagation du prédicat, bugs, et messages d'erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2234 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Solution partielle au problème des alias dépendants pour les rendre ↵herbelin
compatibles avec l'utilisation de la contrainte de type comme guide de la synthèse du prédicat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2229 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Prise en compte des coercions pour typer les branches lorsqu'il y a une ↵herbelin
contrainte de type sur le résultat du Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2221 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout make_arity_signatureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2219 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Correction bug contrainte de valeur trop restrictive sur le typage du type ↵herbelin
du Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2214 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Bug mauvaise instanceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2212 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Bug nommage des fonctions définies par récursion mutuelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2205 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 20:29:32 +0000