aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
AgeCommit message (Collapse)Author
2007-05-17Nettoyage et standardisation des messages d'erreurs.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-09Suppresion de la catégorie des inductifs singletons larges dontherbelin
l'élimination vers Set était autorisée: comme souligné par Benjamin, c'est incompatible avec EM + AC (report rev 9633 8.1) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Correction du bug #1273 (problème avec les paramètres non récursivement ↵notin
uniformes dans le cas de types mutuellement inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9445 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
(suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Correction de 2 bugs critiques du polymorphisme d'universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9301 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28- Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesherbelin
(i.e. cachées sous un nom de constante) sont considérées comme monomorphes. - Divers: renommage type_of_applied_inductive, un peu de documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8871 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
- prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-13Correction trou de typage des éliminations d'inductifs introduit dans ↵herbelin
commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8811 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22- Correction bug calcul mind_consnrealargs, introduit à la révisionherbelin
7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-18Bug calcul consnrealargs + bug calcul occurrences non positives + modifs ↵herbelin
cosmétiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8644 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-20*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7899 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-10Ajout de la longueur de l'arité des constructeurs dans one_inductive_body ↵herbelin
et dans case_info pour permettre l'indépendance de detyping (entre autres) envers l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7833 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵herbelin
et suite correction bug #1028 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-28parametres inductifsmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7620 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Suppression code inactif et commentaire apparemment incorrect (pour éviter ↵herbelin
confusions suite à question de CSC) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7360 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-28Correction bug #983herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7176 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Inductive Types : seuls les petits types sont unitairesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5117 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25modif lexer: ident peut commencer par _barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Suppression StronglyClassical, StronglyConstructive devient plus ↵herbelin
concretement ImpredicativeSet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4828 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Message inductive largeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4730 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Set devient predicatif par defautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04suppression du champ mind_singl inutilisé dans mutual_inductive_bodyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3373 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 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-07erreur mineure dans le test des inductifs imbriquesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2461 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-30Reparation erreur de syntaxemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2443 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-29modification de la definition des def inductives unitaires et autorisation ↵mohring
d'elimination sur la sorte Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2442 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-29condition de positivite moins stricte vis-a-vis des parametres (cf bug de ↵barras
Eduardo) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2441 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-24Cas LetIn superflu dans check_construct car normalisation préalableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2428 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-16correction de bug avec les mutuels imbriques a plusieurs niveauxbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2401 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-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-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵herbelin
des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 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-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 01:56:42 +0000