aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
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-03-18MAJ documentation en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8647 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-18Documentation mutual_inductive_bodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8645 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-02-16added isProd to term.mli.coq
added elim_scheme to tactics.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8049 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-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-11Suppression résidus code v7 et traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7834 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
2006-01-10Détection var inutile par ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7830 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Uniformisation: extension de la suppression d'un casts dans collapse_app à ↵herbelin
la suppression de cascades de casts (utile pour le 4CT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7680 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-17Orthographe de 'instantiate'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-06j'avais oublie ces deux fichiers.gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7642 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-05correction bug 881.gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7641 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-05changement d'egalite pour le named_context_valgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7640 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-23bug #909: Top n'est cree que si le contexte est videbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7602 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-18petites corrections + contournement bug projectionsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7585 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-08Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7536 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite nouvel avertissement Z de ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7535 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-09-08Simplification message d'anomalieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7352 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-22argument inutilisé de zip: toujours l'identitéletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7313 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 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-07-13reactivation de l optim des fermeturesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7216 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13backtrack modif de knh...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7215 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7211 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-12test du tag de reductionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7208 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-05-23Bug fix for a bug reported by Roland: the function that detects the constantssacerdot
to be expanded during functor application was written supposing that the module had already been checked against its signature. However, this is actually a false hypothesis. The bug fix consists in replacing an "assert false" with the error message that would be obtained type checking the module against its module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7061 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-05Bug affichage graphe universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6994 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-05Code v7 obsoleteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6993 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-05MAJ commentaires et inversion du sens du graphe de contraintes pour ↵herbelin
extensibilité aux contraintes numériques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6992 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Added map_named_contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6737 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moved Indmap and ConstrMap from Libnames to Names for use in Cookingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6736 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Uniformisation de destApplication en destAppherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Uniformisation de destApplication en destApp; simplification decompose_appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6712 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-171. added code to handle the inclusion of inductive types and constructors insacerdot
parameters. 2. however, the code is still not working if the parameters are referenced later on in the module signature. To fix this the representation of terms must be changed to unify references to constants, inductive types and constructors. 3. thus the code above is prefixed by an error that suggest to the user how to avoid the problem right now. Note: the above code has not been commented out to keep it in synch with the other changes in the kernel. However, it is dead code for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6600 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
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-05[ Waiting for a keyword to control expansion during functor application ]sacerdot
When F(X: T) := B is applied to M, M.t in B{M/X} is now delta-expanded only if T.t is an axiom or a parameter. This seems to be the expected behaviour at least for orsay/FSets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6561 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 17:08:49 +0000