aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurGravatar herbelin2003-01-21
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Erreur sur precedent commitGravatar herbelin2003-01-19
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Amélioration choix des noms dans abstract_list_allGravatar herbelin2002-12-30
* code mortGravatar herbelin2002-12-24
* Tentative d'interdire les K-abstractions si allow_K est faux et leGravatar herbelin2002-12-23
* Cas motif universelGravatar herbelin2002-12-22
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21