aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
AgeCommit message (Collapse)Author
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-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-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-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-07petit nettoyage de kernel/inductivebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 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
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-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-19Remise en place du Cast pour Correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2199 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-17User Casts are for helping pretyping, experimentally not to be keptherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2198 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2176 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Introduction d'univers frais dans les types implicites engendrés par le ↵herbelin
prétypage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2172 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation du prétypage à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1936 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-20Normalisation du predicat synthetise pour les Caseclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1798 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Facilites pour le debogguage des univers.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-10Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1738 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02bug Fix signalé par Alexandre (even/odd mal interprété)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1510 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1445 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1377 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug vieux Matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1200 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug prédicat old Case/Matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1176 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bugs calcul du prédicat des Cases et Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1119 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1109 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases ↵herbelin
devient systématiquement dépendent; blindage de certaines erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1096 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1011 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24resolution implicites dans produits (bug)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@944 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@885 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08Insertion de coercion au milieu des applications partielles et propagation ↵herbelin
des contraintes de prétypage vers les sous-termes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@825 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Petit nettoyage de Evarutil et Evarconvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@735 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-19Nettoyage Coercionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@732 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec ↵herbelin
sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Renommage canonique :herbelin
declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-13Suppression d'un test inutile dans RCastherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@707 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de Let dans build_dependent_inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:35:51 +0000