aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.mli
Commit message (Expand)AuthorAge
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Types inductifs parametriquesGravatar mohring2005-11-02
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Export de l'information si un inductive est un record ou non (pour xml)Gravatar herbelin2004-03-31
* Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...Gravatar herbelin2004-01-29
* Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...Gravatar herbelin2004-01-13
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Mise en place structure pour des 'arguments scope' dirigés par une classeGravatar herbelin2003-06-10
* Possibilité de syntaxe conjointement à la définition des inductifs et des ...Gravatar herbelin2003-05-21
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Clarification changements autour de Remark/Fact/LocalGravatar herbelin2002-10-23
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourGravatar herbelin2002-07-11
* Intgration uniforme de coercions dans les dclarations (Variable and co) et re...Gravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Meilleure gestion de la reduction dans FieldGravatar delahaye2002-03-17
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* ParsingGravatar herbelin2001-08-10
* Uniformisation des 'Save def_tok id'Gravatar herbelin2001-04-09
* entetesGravatar filliatr2001-03-15
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Réorganisation suite ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Découpage des différentes fonctionnalités de build_mutual et definition_st...Gravatar herbelin2000-12-19
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Distinction local/globalGravatar herbelin2000-11-27
* Renommage canonique :Gravatar herbelin2000-10-18
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* export get_current_contextGravatar herbelin2000-05-18
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Nettoyage des fichiers de parsingGravatar herbelin2000-01-13
* Les inductifs dans Scheme doivent être des ident d'inductifsGravatar herbelin1999-12-15
* documentation interfacesGravatar filliatr1999-12-13
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* module CommandGravatar filliatr1999-12-02
* module MetasyntaxGravatar filliatr1999-12-01