aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
Commit message (Expand)AuthorAge
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* gestion speciale du niveau 5 des ltacGravatar barras2006-11-02
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...Gravatar herbelin2006-01-09
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Added entry constr_may_eval for tactic extensions (new syntax)Gravatar herbelin2005-06-22
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-25
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* Uniformisation du nom d'entrée openconstr en le nom du type open_constrGravatar herbelin2004-12-06
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...Gravatar herbelin2004-03-02
* Généralisation du type ltac Identifier en IntroPattern; prise en compte des...Gravatar herbelin2004-03-01
* Ajout de lconstr, constr et binder_constr dans Print Grammar constrGravatar herbelin2004-02-17
* Nouvelle tactique EExistsGravatar clrenard2003-12-01
* Ajout ne_stringGravatar herbelin2003-11-27
* Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...Gravatar herbelin2003-11-20
* Protection contre l'effacement des niveaux vides de operconstr et pattern par...Gravatar herbelin2003-11-19
* New tactics : econstructor, eleft, eright, esplitGravatar clrenard2003-11-17
* Fusion de tuple_constr/tuple_pattern dans operconstr/patternGravatar herbelin2003-11-08
* Extension de get_constr_entry et symbol_of_production pour gerer les extensio...Gravatar herbelin2003-11-01
* On n'autorise plus les niveaux doubles L/R en v8Gravatar herbelin2003-10-17
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Parsing au niveau lconstr des patterns de 'match context'Gravatar herbelin2003-09-21
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Meilleure factorisation des entrées NEXT internesGravatar herbelin2002-12-15
* Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...Gravatar herbelin2002-12-04
* On force l'associativité pour les entrées sans niveauxGravatar herbelin2002-12-02
* Utilisation de Snext pour gérer les symboles non associatifsGravatar herbelin2002-11-29
* Ajout d'une entre Prim.bigintGravatar herbelin2002-11-28
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
* 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
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
* Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageGravatar herbelin2002-10-13
* passage a ocaml 3.06Gravatar herbelin2002-09-27
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Ajout de l'entrée ne_constrarg_listGravatar delahaye2002-03-19
* Meilleure gestion de la reduction dans FieldGravatar delahaye2002-03-17