aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Retire le warning statGravatar mohring2001-02-02
* retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...Gravatar filliatr2001-02-02
* Nouvelle betaGravatar herbelin2001-02-02
* bug Variable + RecordGravatar filliatr2001-02-01
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* *** empty log message ***Gravatar mohring2001-02-01
* Reparation reduce_to_mindGravatar mohring2001-02-01
* oubli de Closure.EvalConstRefGravatar filliatr2001-02-01
* - coqc : option -imageGravatar filliatr2001-02-01
* Bug localisation des Syntactif DefinitionGravatar herbelin2001-01-31
* MAJGravatar herbelin2001-01-31
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Bug lié au dischargeGravatar herbelin2001-01-31
* MAJGravatar herbelin2001-01-31
* Ajout option Set/Unset/Test Printing CoercionsGravatar herbelin2001-01-31
* Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...Gravatar herbelin2001-01-31
* Prise en compte du let-in dans lookup_*_as_renamedGravatar herbelin2001-01-30
* MAJGravatar herbelin2001-01-30
* MAJGravatar herbelin2001-01-30
* Les Objdef introduisent une convertibilité avec les projections dans le test...Gravatar herbelin2001-01-30
* Branchement sur ObjdefGravatar herbelin2001-01-30
* Les Objdef introduisent une convertibilité avec les projections dans le test...Gravatar herbelin2001-01-30
* Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_mainGravatar sacerdot2001-01-30
* backtrack sur le lexeur de la V6Gravatar filliatr2001-01-30
* pas de warning avec Opaque quand is_silentGravatar filliatr2001-01-29
* As an heuristic, now both in tauto and intuition we try to avoid the initialGravatar sacerdot2001-01-29
* make docGravatar herbelin2001-01-27
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
* Simplification ImpargsGravatar herbelin2001-01-27
* Suppression du retrait du répertoire doc de l'archive tar-gzip-éeGravatar herbelin2001-01-27
* Ajout alias mutual_inductive_path = section_pathGravatar herbelin2001-01-27
* Factorisation du '.' finalGravatar herbelin2001-01-27
* make docGravatar herbelin2001-01-27
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
* Modif de l'axiomatisation pour enlever les /\ de _neGravatar mayero2001-01-25
* Remplacement d'un bug non documente par un autre documente dans quantify_extr...Gravatar herbelin2001-01-25
* Ajout flush, diversGravatar herbelin2001-01-24
* MAJGravatar herbelin2001-01-24
* Protection contre l'échec de Unix.statGravatar herbelin2001-01-24
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Prise en compte des noms longs dans les Hints et les CoercionsGravatar herbelin2001-01-24
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* MAJGravatar herbelin2001-01-24
* Ajout global_vars_declGravatar herbelin2001-01-24
* Réorganisation suite ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* DocGravatar herbelin2001-01-24
* Ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Retour en arrière sur le pb f_equal en attente meilleure solutionGravatar herbelin2001-01-22
* Tests pourGravatar herbelin2001-01-21
* Bug « f_equal » : arguments inférables par une unification des types qui n...Gravatar herbelin2001-01-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-21 19:59:11 +0000