aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
* code mortGravatar herbelin2002-12-21
* Prise en compte des coercions dans les 'with' bindingsGravatar herbelin2002-12-20
* simplification de solve_subgoal: n'utilise plus frontierGravatar barras2002-12-19
* suite du commit precedentGravatar barras2002-12-19
* Compensation de suppression betaiota de type_of (suite)Gravatar herbelin2002-12-13
* Compensation de suppression betaiota de type_of (suite)Gravatar herbelin2002-12-12
* Ajout du vernac Proof withGravatar gregoire2002-12-12
* Compensation de suppression betaiota de type_ofGravatar herbelin2002-12-11
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* simplification common_ancestorGravatar courant2002-11-13
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesGravatar herbelin2002-10-21
* NewDestruct/NewInduction acceptent l'option "using"Gravatar herbelin2002-10-21
* L'application de ltac attend une référence; meilleure protection contreGravatar herbelin2002-10-14
* Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageGravatar herbelin2002-10-13