aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Collapse)Author
2000-10-26Require Export recursifsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@768 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Bug pop_path_prefix : List.rev manquantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@760 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23L'état implicite des définitions survivant au discharge redevient celui du ↵herbelin
moment de la définition (et non celui du moment de la fermeture de section) mais les args imps sont recalculés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@740 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23module_segment et module_filenamefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@739 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec ↵herbelin
sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Renommage canonique :herbelin
declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@724 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de l'environnement dans le calcul des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@692 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de Let dans build_dependent_inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06correction bug univers (dummy_univ)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@664 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Chasse aux de-cast inutilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@626 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@612 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Abstraction de constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Intégré à Tacredherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@601 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Suppression de Abstherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@592 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. ↵herbelin
Abstraction de constr. LetIn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@589 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@588 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-08-21Nametab.init - bug correctedcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@581 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-25retablissement make doc et make minicoqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 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-01Précalcul de la forme canonique des constructeurs et arités pour traiter ↵herbelin
les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> ↵filliatr
.vo plus petits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@514 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@485 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-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Amélioration capture des erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@479 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Bugs d'index d'inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@466 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-18Adaptation pour nouveaux inductifs (cf Inductive)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@440 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-03suppression de Fw pour les implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@405 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-02construct_reference prend en compte aussi les variables du contextfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@399 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28portage Omega (code seulement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@381 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-21discharge des axiomesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@366 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@363 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@351 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
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-20Broutillesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@278 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Correction pbs liés aux evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@265 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14sauvegarde de la valeur de module_namefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@253 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-01 07:04:58 +0000