aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Export du type de preuve en cours pour xmlGravatar herbelin2004-03-29
* Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...Gravatar herbelin2004-03-02
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
* added breakpoints to help ideGravatar corbinea2004-02-26
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
* bugs avec Pose et AssertGravatar barras2004-01-09
* Bug affichage des metas dans un environnement avec definitions locales (bug 277)Gravatar herbelin2003-12-19
* Amélioration du message d'erreur "w_unify"Gravatar clrenard2003-12-01
* Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...Gravatar herbelin2003-11-25
* Prise en compte des defs syntaxiques dans is_global et global_reference qui p...Gravatar herbelin2003-11-24
* Amelioration du message d'erreur en cas de tentative d'instanciationGravatar clrenard2003-11-15
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* petits changements de syntaxeGravatar barras2003-11-12
* Traduction semantique des InHyp de clause en InHypValue si local defGravatar herbelin2003-11-09
* Ajout pf_applyGravatar herbelin2003-11-09
* Added Instantiate ... inGravatar corbinea2003-11-06
* 2 espaces en tropGravatar herbelin2003-11-05
* Amelioration de l'afficheur de script structureGravatar herbelin2003-11-05
* nouvelle syntaxe de ltacGravatar barras2003-10-16
* code mortGravatar herbelin2003-10-10
* pf_get_new_id en provenance de feu wcclausenvGravatar herbelin2003-10-10
* Suppression clenv_change_head que seul Wcclausenv utisaitGravatar herbelin2003-10-10
* Cablage en dur de inversionGravatar herbelin2003-10-10
* Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...Gravatar herbelin2003-10-10
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* open superfluGravatar herbelin2003-09-12
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Ground updateGravatar corbinea2003-07-08
* Ground Update.Gravatar corbinea2003-06-20
* Ajout 'Symmetry in Hyp'Gravatar herbelin2003-06-19
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
* Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...Gravatar herbelin2003-06-10
* Ajout FreshIdGravatar herbelin2003-05-24
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* coqide: toolbar/autosaveGravatar monate2003-05-07
* Localisation erreurs TacAlias; Globalisation moins tolérante dans lesGravatar herbelin2003-04-28
* Localisation des appels de tactiques définies sans argumentsGravatar herbelin2003-04-14
* 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
* Réparation bug de l'unification. En effet, avant l'instanciation d'une evarGravatar clrenard2003-03-28
* *** empty log message ***Gravatar barras2003-03-12
* Debugger plus informatifGravatar delahaye2003-02-13
* Bug RenameGravatar herbelin2003-02-08