aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.mli
Commit message (Collapse)AuthorAge
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
| | | | | | | | | | splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
| | | | | | | | | | | | | | | | | contraintes bornant par le haut le type de l'inductif (ce qui peut arriver quand l'inductif est argument d'une constante) étaient oubliées : on pouvait se retrouver avec des inductifs dont le type des constructeurs, une fois instancié par des paramètres) n'était plus typable (seul leur réduit, après expansion des constantes, était typable). [kernel, test-suite] + Affichage des inductifs (via Print) en prenant la forme utilisateur des constructeurs. + Correction warning dans compilation gallina.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug condition de gardeGravatar barras2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
| | | | | | | | | Amélioration affichage des univers. Réparation de petits oublis du premier commit. Essai d'une nouvelle stratégie : si le type d'une constante est mentionné explicitement, la constante est monomorphe dans Type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
| | | | | | | | | | (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
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
| | | | | | | | | | | | | | | | | | | Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
| | | | | | | | | (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
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - 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
* correction bugs de condition de garde (fix + cofix)Gravatar barras2006-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
| | | | | | | | | 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
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration messages d'erreur arité incorrecte (notamment record)Gravatar herbelin2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2236 85f007b7-540e-0410-9357-904b9bb8a0f7
* types vs constrGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour make docGravatar herbelin2001-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2177 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - 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
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵Gravatar herbelin2001-09-19
| | | | | | des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵Gravatar herbelin2001-09-10
| | | | | | é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
* nettoyage extractionGravatar filliatr2001-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-Déplacement extended_rel_listGravatar herbelin2001-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1423 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle implantation de la reductionGravatar barras2001-03-01
| | | | | | | suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un système optionnel de discharge immédiat; prise en ↵Gravatar herbelin2001-02-14
| | | | | | 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
* make docGravatar herbelin2001-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1286 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifications autour de typed_type (renommé types par analogie avec ↵Gravatar herbelin2000-10-18
| | | | | | sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pb de globalisation dans print_mutualGravatar herbelin2000-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des find_m*typeGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Précalcul de la forme canonique des constructeurs et arités pour traiter ↵Gravatar herbelin2000-07-01
| | | | | | 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
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@542 85f007b7-540e-0410-9357-904b9bb8a0f7
* docGravatar herbelin2000-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
| | | | | | | | | | | | | | - 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
* Ajout mis_typepathGravatar herbelin2000-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait fullmind de inductive_summary pour simplicitéGravatar herbelin2000-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des fonctions de formation du 'case_info'; Suppression de make_arity ↵Gravatar herbelin2000-03-21
| | | | | | et make_constructor de inductive_summary git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@333 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 01:51:57 +0000