aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Ajout syntaxe concrète Proposition, synonyme de LemmaGravatar herbelin2006-01-29
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* - Ajout syntaxe concrète Property/Corollary, synonymes de LemmaGravatar herbelin2006-01-28
* *** empty log message ***Gravatar barras2006-01-20
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Tentative de réparation du bug #1025: it seems like that a casted module sho...Gravatar herbelin2005-12-24
* Vérification qu'un module est ouvert avant d'insérer une déclaration nommÃ...Gravatar herbelin2005-12-23
* Changement des named_contextGravatar gregoire2005-12-02
* Fonctionnalisation du cache 'compunit' pour réparer correctement le bug #103...Gravatar herbelin2005-11-26
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Conformité au principe du nouveau warning X de ocaml 3.09Gravatar herbelin2005-11-04
* Types inductifs parametriquesGravatar mohring2005-11-02
* Correction bug #1030 (conséquence du commit 1.84 sur le discharge: add_froze...Gravatar herbelin2005-11-01
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Keep ClosedSection marker for resetGravatar herbelin2005-02-20
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...Gravatar herbelin2005-02-18
* Code mortGravatar herbelin2005-02-18
* Ajout du reset des numéros d'états dans reset_initial. Plus propreGravatar coq2005-02-10
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Localisation des libraries compilées uniquement via la structure du loadpath...Gravatar herbelin2005-02-05
* Petit changement dans la gestion des nouveaux labels d'état (pour leGravatar coq2005-01-31
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Ajout mémorisation numéro commande courante + reset vers ce numéro pour mo...Gravatar herbelin2005-01-14
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* HUGE COMMITGravatar sacerdot2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Bug 'Locate Library lib' quand 'lib' est aussi un moduleGravatar herbelin2004-11-17
* dead (and obsolete) code (in comments) removedGravatar sacerdot2004-11-16
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* code mortGravatar herbelin2004-11-09
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...Gravatar herbelin2004-10-12
* option -no-hash-consing pour supprimmer le hash-consingGravatar filliatr2004-10-12
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #780: compilation of several units in the same coqtop processGravatar barras2004-07-13
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* MAJ numéro magiqueGravatar herbelin2004-04-14
* Export de l'information si un inductive est un record ou non (pour xml)Gravatar herbelin2004-03-31
* The XML exportation hook for require is now active for:Gravatar sacerdot2004-03-30
* Distinction entre declarations internes (p.ex. _subproof) et declarations uti...Gravatar herbelin2004-03-30
* Crocret xml pour RequireGravatar herbelin2004-03-29
* Crochets pour exported les sections en xmlGravatar herbelin2004-03-27