aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
Commit message (Collapse)AuthorAge
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7602 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 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
* Suppression StronglyClassical, StronglyConstructive devient plus ↵Gravatar herbelin2003-11-08
| | | | | | concretement ImpredicativeSet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Set devient predicatif par defautGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un mecanisme ne chargeant pas les preuves opaquesGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contexte locale non-vide interdit a la fin d'un module ou module typeGravatar coq2002-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3453 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du hash-consing vers declare.mlGravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrections de gestion des univers et modules + meilleure gestions des ↵Gravatar coq2002-12-09
| | | | | | noms uniques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy manuelles dans le codeGravatar coq2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy experimentale temporaire...Gravatar coq2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Activation du hash-consingGravatar herbelin2002-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3049 85f007b7-540e-0410-9357-904b9bb8a0f7
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 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 modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
* resolution du pb d'efficacite du a Sign.add_named_declGravatar barras2002-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de pop_namedGravatar barras2002-02-22
| | | | | | | meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
| | | | | | | | + 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
* Oubli des contraintes d'univers lors de la suppression des cast dans un ↵Gravatar herbelin2001-11-21
| | | | | | commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des Cast externes dans les définitionsGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2208 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'une méthode directe pour indiquer le type des déclarations ↵Gravatar herbelin2001-11-19
| | | | | | à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 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 option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 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
* repare la perte d'opacite a la fermeture de sectionGravatar barras2001-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2050 85f007b7-540e-0410-9357-904b9bb8a0f7
* TransparentGravatar barras2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage aux univers algébriquesGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mécanisme pour faire remonter les contraintes de typage sur les variables ↵Gravatar herbelin2001-09-09
| | | | | | de section au niveau du discharge, sans avoir à garder tout l'environnement de la section; suppression retypage du type des constantes déchargées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1935 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
| | | | | | | 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
* Changement de la structure des points fixesGravatar barras2001-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
* un typage sûr pour Goal et CheckGravatar filliatr2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1647 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de la structure des universGravatar barras2001-03-28
| | | | | | | | elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 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
* réparation (?) discharge axiomeGravatar filliatr2001-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1432 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
* Changement de subst_metaGravatar mohring2001-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 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
* - suppression mind_extract_paramsGravatar filliatr2000-12-15
| | | | | | | | | - contraintes univers parametres inductifs prises en compte - exception UniverseInconsistency donne un message "Error: Universe Inconsistency" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite réorganisationGravatar herbelin2000-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les params d'inductif deviennent en même temps propre à chaque inductif ↵Gravatar herbelin2000-12-14
| | | | | | 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@1110 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
* Prise en compte de la contrainte de type dans Definition comme étant un ↵Gravatar herbelin2000-11-29
| | | | | | cast de l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans le calcul des dépendances dans add_discharged_constantGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation bug mutuels indGravatar mohring2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@916 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵Gravatar filliatr2000-11-06
| | | | | | constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 11:15:59 +0000