aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Collapse)Author
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-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-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-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵herbelin
par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1860 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-05Re-Déplacement extended_rel_listherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1423 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28Changement de subst_metamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 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
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1113 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-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-18Correction pb de globalisation dans print_mutualherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@715 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Renommage des find_m*typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@693 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
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Suppression de ensure_applherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@631 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Abstraction de constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter ↵herbelin
les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@545 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@542 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-03Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@500 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Restructuration des outils pour les inductifs.herbelin
- Les déclarations (mutual_inductive_packet et mutual_inductive_body), utilisisées dans Environ vont dans Constant - Instantiations du context local (mind_specif), instantiation des paramètres globaux (inductive_family) et instantiation complète (inductive_type, nouveau nom de inductive_summary) vont dans Inductive qui est déplacé après réduction - Certaines fonctions de Typeops et celle traitant des inductifs dans Reduction sont regroupées dans Inductive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@438 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-16Ajout mis_typepathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@435 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-27Retrait fullmind de inductive_summary pour simplicitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@376 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Ajout des fonctions de formation du 'case_info'; Suppression de make_arity ↵herbelin
et make_constructor de inductive_summary git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@333 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-08Peaufinement nouveaux types inductive_summary et constructor_summary en vueherbelin
de remplacer mispec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@301 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10debug discharge et inductifsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@227 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09Ajout des messages d'erreurs de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@226 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-06declarations eliminations / debuggae inductifs (debut)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@212 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-05explicitations erreurs inductifsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@203 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26Modification pour faire compiler pretyping.ml qui maintenant compileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@156 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-22module Wcclausenvfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@130 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-22module Tactics (debut)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@129 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-19module Pattern, Wcclausenv (interface) et Tacticalsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-25ensembles de contraintes d'universfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-27suppression champs inutiles dans constantes et inductifs; verification ↵filliatr
definitions inductives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@29 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-26environnement surfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@28 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-25modules Instantiate, Constant et Inductivefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@22 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:04:12 +0000