aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_proofs.ml4
Commit message (Expand)AuthorAge
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Nouvelle en-têteGravatar herbelin2004-07-16
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Debranchement de l'affichage automatique de Proof par le traducteur (trop com...Gravatar herbelin2003-10-07
* Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...Gravatar herbelin2003-09-12
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
* Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun impliciteGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Ajout du vernac Proof withGravatar gregoire2002-12-12
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...Gravatar herbelin2002-11-24
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourGravatar herbelin2002-07-11
* Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructGravatar herbelin2002-06-05
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Retablissement de la commande Existential que j'avais supprime par erreur.Gravatar clrenard2001-11-23
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
* Prise en compte qualid dans Hint UnfoldGravatar herbelin2001-09-13
* ajout Show Intro(s)Gravatar letouzey2001-07-04
* Fix de quelques bugs syntaxiques de LtacGravatar delahaye2001-06-11
* Uniformisation des 'Save def_tok id'Gravatar herbelin2001-04-09
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* entetesGravatar filliatr2001-03-15
* Factorisation du '.' finalGravatar herbelin2001-01-27
* Prise en compte des noms longs dans les Hints et les CoercionsGravatar herbelin2001-01-24
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Nouveau mode de compilation de .ml4Gravatar herbelin2000-11-05
* Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...Gravatar herbelin2000-11-05