aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-06kernel/type_errors.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@583 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-08-08reparation bug des coercions (cas ou on importe une coercion faisantbarras
reference a une classe non importee) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@577 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-21Modifs d'interpretation de patternsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@562 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-20portage Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@546 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-07-01index devenu list_index échoue maintenant avec Not_found et plus Failureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@540 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
Contournement des dépendances de Rel dans les Evar pour l'inférence du prédicat (erreur "TODO4-1") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@538 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@532 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Séparation des contraintes de type et de valeur dans pretypingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@531 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Bricolesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@526 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Extension de l'inférence des types des lambdas du prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@524 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Achèvement abstraction du mécanisme (optionnel) de castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@523 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-28Rattrapage d'un Not_found pour les VAR's.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@519 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-09Bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@503 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-09Amelioration messages erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@502 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02bugs infrence des arguments manquants dans le prdicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@494 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02bugs et simplification (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@493 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Bugs et simplifications coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@487 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-31Afficahge des locationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@483 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Genericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans ↵herbelin
les instances de références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@476 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-23Bug de castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@474 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Rienherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@467 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-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@442 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Réorganisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@424 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@416 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03diverses modifs pour ocamlwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout du langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-02pattern-matching non-exhaustif (occur_rawconstr)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@398 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@394 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Déplacement du type reference dans Termherbelin
Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@384 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 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-26renommage ancien pattern en cases_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@370 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26N'importe quel rawconstr maintenant dans le contexte d'une référenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@369 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 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-28Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en ↵herbelin
interp_constr etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@356 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Modification de type_of_case, type_case_branches, etcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@352 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Prise en compte nouveau case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@343 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Plus besoin de env dans reduce_mind_caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@338 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Inlining prod_createherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@336 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Prise en compte nouveau case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@334 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-25 13:36:37 +0000