aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/omega/coq_omega.ml
Commit message (Expand)AuthorAge
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* commentairesGravatar herbelin2003-04-17
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* minus a changé d'emplacement -> omega pas contentGravatar letouzey2003-03-31
* *** empty log message ***Gravatar barras2003-03-12
* Problèmes et améliorations divers affichageGravatar herbelin2002-12-09
* Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...Gravatar herbelin2002-10-23
* Meilleure lisibilité grâce à tclTHENLISTGravatar herbelin2002-10-19
* Réparation bug #180Gravatar herbelin2002-10-19
* Omega can now elim hyps of type False. Therefore, it knows how to dealGravatar courant2002-10-02
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Protection des tactiques contre l'utilisation sans le bon contexte de thoriesGravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlGravatar herbelin2002-04-11
* Uniformisation convert_hypGravatar herbelin2002-02-28
* patch Omega (bug 129)Gravatar filliatr2002-01-25
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* correction bug OmegaGravatar filliatr2001-07-05
* remplace Zarith par ZArithGravatar mohring2001-04-19
* portage exemples Correctness; changement du nom de pred_of_minus dans coq_omegaGravatar filliatr2001-04-10
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Changement dans les noms longs (2eme)Gravatar herbelin2000-11-29
* Changement dans les noms longsGravatar herbelin2000-11-29
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* id_of_global devient sp_of_globalGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* Nettoyage Names suiteGravatar herbelin2000-11-07
* Renommage AppL en AppGravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* MODIFS pour compatibilité aussi 2.99Gravatar herbelin2000-04-30
* mise sous CVS d'OmegaGravatar filliatr2000-04-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 22:28:39 +0000