aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
Commit message (Expand)AuthorAge
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Implementation of a new backtracking system, that allow to go backGravatar coq2005-04-20
* Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...Gravatar herbelin2004-12-31
* Code mortGravatar herbelin2004-11-18
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* Export du type de preuve en cours pour xmlGravatar herbelin2004-03-29
* Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...Gravatar herbelin2003-10-10
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* open superfluGravatar herbelin2003-09-12
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* Ajout du vernac Proof withGravatar gregoire2002-12-12
* 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
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Ajout d'un point d'entree pour exporter les arbres de preuves en XMLGravatar herbelin2002-07-24
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* changement de l'undo limitGravatar barras2002-04-03
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* TransparentGravatar barras2001-09-20
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Code mortGravatar herbelin2000-12-20
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* 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
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Achèvement nettoyage PfeditGravatar herbelin2000-05-05
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...Gravatar herbelin2000-03-28
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* - méthode load sur les HintsGravatar filliatr1999-12-13
* - erreurs PretypeGravatar filliatr1999-12-10
* debug resetGravatar filliatr1999-12-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 07:40:55 +0000