aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* 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
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* Vraie substitutivite de autohintsGravatar coq2002-10-01
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Ajout d'un point d'entree pour exporter les arbres de preuves en XMLGravatar herbelin2002-07-24
* MAJ commentairesGravatar herbelin2002-07-23
* Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...Gravatar herbelin2002-07-11
* CommentairesGravatar herbelin2002-06-14
* Bug non vérification non redondance par CutGravatar herbelin2002-06-13
* Déplacement de proofs vers tacticsGravatar herbelin2002-05-29
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Réorganisation des tclTHEN (cf dev/changements.txt)Gravatar herbelin2002-05-29
* Fichier des expressions de tactiquesGravatar herbelin2002-05-29
* Ajout de Eval, Inst et CheckGravatar delahaye2002-05-27
* Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deGravatar herbelin2002-05-15