aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/name_to_ast.ml
Commit message (Expand)AuthorAge
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* removes several warnings in contrib/interfaceGravatar bertot2006-01-11
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* make sure the implicit argument indications are in the right orderGravatar bertot2004-03-03
* 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
* Conjecture declare maintenant un axiome; reorganisation VernacDefinitionGravatar herbelin2003-10-23
* Mise en place possibilité de définitions locales dans les paramètres des i...Gravatar herbelin2003-09-06
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* Ajout du traducteurGravatar desmettr2003-02-05
* removes all references to ctast.ml the Makefile has been updated accordingly.Gravatar bertot2003-01-22
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Des critères plus fins d'analyse des implicites automatiques; meilleur affic...Gravatar herbelin2002-10-28
* Lazy manuelles dans le codeGravatar coq2002-10-07
* correcting the treatment of many tactics that use quant_hyp in file xlate.mlGravatar bertot2002-10-06
* 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
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Renommage qualid_of_global en shortest_qualid_of_globalGravatar herbelin2001-11-19
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* TransparentGravatar barras2001-09-20
* PrsingGravatar herbelin2001-08-10
* Pretty -> PrettypGravatar filliatr2001-05-28
* Files that handle the dialogue with the graphical user-interface pcoq.Gravatar bertot2001-04-04