aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Collapse)Author
2006-12-12cosmetiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9442 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08bug condition de gardebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9420 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-30Débranchement du polymorphisme de sorte sur les définitions dans Typeherbelin
(trop de problèmes à régler, comme par exemple des types identiques qui se retrouvent dans des sortes disjointes, résultant en davantage d'équations (eq Type(i) a b) et (eq Type(j) a b) avec i syntaxiquement distinct de j, que Coq ne sait en général pas traiter -- i.e. ne sait pas forcer i==j (cf contrib CatsInZF: échec du test "dependent" dans "rewrite"); autre problème: le ralentissement du prouveur (logic.ml)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9323 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
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
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-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug #1242) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
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
2006-06-22Correction bug du polymorphisme de sort des inductifs (cas où les variables ↵herbelin
d'univers associées aux arités des paramètres ne sont pas distinctes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8972 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-12correction bugs de condition de garde (fix + cofix)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8810 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-09subst. explicites avec vecteursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8799 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-03fixed bug #804: removed useless reduction in fix guard checkingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8784 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 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-01-21Variable inutiliséeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7914 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-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-07-21Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ↵herbelin
CP et EC dans coqdev) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7250 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-12-06Commentaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6409 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-06Amélioration message d'erreur objet de récursion de type non inductifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6019 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-05-27Un bug résiduel (mais pas bien méchant) du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5767 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22message d'erreur de garde des cofixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4438 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18bug fix: term reduced in bad envbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4407 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵letouzey
list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-18- amelioration des messages d'erreur de la condition de gardebarras
- restructuration de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3455 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-04-03renommage de l'exception locale Aritybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2606 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-29*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2576 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-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-05evaluable_constant retournait vrai pour les constantes opaques, ce qui faisaitbarras
boucler la condition de garde git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2454 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-12-20Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2353 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Bug de de Bruijn pour le LetInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2348 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Le cas LetIn avait été oublié dans case_branches_specifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2324 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-10- condition de garde (suite)barras
- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-04bug fix de la condition de gardebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2264 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30desobfuscation du code de la verif de la condition de gardebarras
reparation bug de la tactique CutRewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2261 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 02:04:29 +0000