aboutsummaryrefslogtreecommitdiff
path: root/library/lib.ml
AgeCommit message (Collapse)Author
2001-07-05Avertissement contre les Require dans le corps d'une sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1829 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28bug Reset et Sectionsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1410 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Test pour empêcher 2 sections de même nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1172 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Pédagogieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1152 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bug des locaux au premier niveau des modules qui disparaissaient de ↵herbelin
l'environnement (changement de is_section_p) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1120 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Reparation conditions de positivites inductifs, echange dans add_entrymohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29La zone par défaut pour le nommage des modules est Scratchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1018 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath ↵herbelin
pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon ↵filliatr
Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21reset_name: try / with juste autour de find_entry_p (=> propage lesfilliatr
vraies erreurs de reset_to s'il y en a) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@908 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21ajout d'un frozen_state après la fermeture d'une section (sinon bug !)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@906 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21correction bug Resetfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@898 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ↵filliatr
variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Petit bug entre close_section'sherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@894 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique ↵herbelin
export_objet aussi aux sections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@861 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15methode exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵herbelin
DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 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-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-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-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
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
1999-12-13mise a jour de refiner.ml (reports de modifs de la V6.3)barras
bug possible dans lib.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@250 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12modulesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10debug resetfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09 - constantes avec recettesfilliatr
- discharge en deux temps, avec état remis comme au début de la section (mais c'est toujours buggé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-08deplacement de Discharge dans toplevelfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-05add_leaf -> application methode cachefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@204 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02modifs pour premiere edition de liensfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01make_strength / reset_libraryfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@171 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-29portage Astterm (partiellement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-29with_heavy_rollback deplace dans Statesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@89 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-28juste l'interface de Dischargefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@85 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-19module Declarefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-19 - un effort sur la doc (ocamlweb)filliatr
- module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-18module Libraryfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-10modules System, Lib et Statesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@71 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 06:09:43 +0000