aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.ml
Commit message (Expand)AuthorAge
* Bug affichage des metas dans un environnement avec definitions locales (bug 277)Gravatar herbelin2003-12-19
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* 2 espaces en tropGravatar herbelin2003-11-05
* Amelioration de l'afficheur de script structureGravatar herbelin2003-11-05
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Ground updateGravatar corbinea2003-07-08
* Ground Update.Gravatar corbinea2003-06-20
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Affichage des tactiques en v8Gravatar herbelin2003-04-07
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* simplification de solve_subgoal: n'utilise plus frontierGravatar barras2002-12-19
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...Gravatar herbelin2002-07-11
* Réorganisation des tclTHEN (cf dev/changements.txt)Gravatar herbelin2002-05-29
* prterm -> prterm_envGravatar filliatr2002-02-08
* compat ocaml 3.03Gravatar filliatr2001-12-13
* suppression de l'affichage des noeuds Change_evarsGravatar barras2001-12-11
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Problème d'affichage d'un . pour les Local_constraints; remplacement par IdtacGravatar herbelin2001-09-21
* exceptionsGravatar barras2001-09-14
* Suppression de l'affichage du non-reparsable 'Local constraint change'Gravatar herbelin2001-07-24
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Metas dans les Unfold'sGravatar delahaye2001-04-19
* Reparation du bug de TryGravatar delahaye2001-04-14
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* introduction d'un refine avec resolution des types et de l'instantiation des ...Gravatar mohring2001-02-28
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* Remplacement de debug en assertGravatar herbelin2000-12-25
* Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...Gravatar herbelin2000-12-20
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Essai de remplacement du whd_betaiotaevar de Qed par un whd_iseGravatar herbelin2000-10-26
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Code redondantGravatar herbelin2000-10-13
* Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)Gravatar herbelin2000-10-04
* Utilisation de local_strong plutôt que strong buggé avec défs localesGravatar herbelin2000-10-04
* Correction pour make docGravatar herbelin2000-09-10
* 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
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 15:33:19 +0000