| Age | Commit message (Expand) | Author |
|---|
| 2008-05-26 | Résolution bug #1850 sur notations avec niveaux inconnus de | herbelin |
| 2008-05-11 | - Cleanup parsing of binders, reducing to a single production for all | msozeau |
| 2008-05-06 | Postpone the search for the recursive argument index from the user given | msozeau |
| 2008-04-30 | Contournement laborieux de la "feature" de camlp5 qui entrainait le | herbelin |
| 2008-04-26 | Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour | herbelin |
| 2008-03-06 | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau |
| 2008-01-15 | Generalize instance declarations to any context, better name handling. Add ho... | msozeau |
| 2008-01-07 | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-09-28 | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu |
| 2007-09-15 | * Adding compability with ocaml 3.10 + camlp5 (rework of | letouzey |
| 2007-04-28 | Ajout de la possibilité de faire référence dans certains cas à un nom | herbelin |
| 2006-11-20 | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin |
| 2006-11-02 | gestion speciale du niveau 5 des ltac | barras |
| 2006-09-20 | Declarative Proof Language: main commit | corbinea |
| 2006-06-08 | Changement du type d'argument 'TacticArgType X' en un type | herbelin |
| 2006-06-07 | Correction trou de subject-reduction de create_arg dans genarg.mli | herbelin |
| 2006-01-09 | Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement... | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-06-22 | Added entry constr_may_eval for tactic extensions (new syntax) | herbelin |
| 2005-05-17 | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin |
| 2005-01-13 | Construct "T with (Definition|Module) id := c" generalized to | sacerdot |
| 2004-12-25 | Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque... | herbelin |
| 2004-12-09 | Restauration type casted_open_constr pour tactique refine car l'unification n... | herbelin |
| 2004-12-06 | Uniformisation du nom d'entrée openconstr en le nom du type open_constr | herbelin |
| 2004-12-06 | Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti... | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-02 | Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no... | herbelin |
| 2004-03-01 | Généralisation du type ltac Identifier en IntroPattern; prise en compte des... | herbelin |
| 2004-02-17 | Ajout de lconstr, constr et binder_constr dans Print Grammar constr | herbelin |
| 2003-12-01 | Nouvelle tactique EExists | clrenard |
| 2003-11-27 | Ajout ne_string | herbelin |
| 2003-11-20 | Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons... | herbelin |
| 2003-11-19 | Protection contre l'effacement des niveaux vides de operconstr et pattern par... | herbelin |
| 2003-11-17 | New tactics : econstructor, eleft, eright, esplit | clrenard |
| 2003-11-08 | Fusion de tuple_constr/tuple_pattern dans operconstr/pattern | herbelin |
| 2003-11-01 | Extension de get_constr_entry et symbol_of_production pour gerer les extensio... | herbelin |
| 2003-10-17 | On n'autorise plus les niveaux doubles L/R en v8 | herbelin |
| 2003-10-10 | changement nouvelle syntaxe (pt fixes) | barras |
| 2003-09-21 | Parsing au niveau lconstr des patterns de 'match context' | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-05-21 | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-03-12 | *** empty log message *** | barras |
| 2002-12-15 | Meilleure factorisation des entrées NEXT internes | herbelin |
| 2002-12-04 | Correction divers bugs d'affichage; explicitation du niveau de grammaire quan... | herbelin |
| 2002-12-02 | On force l'associativité pour les entrées sans niveaux | herbelin |
| 2002-11-29 | Utilisation de Snext pour gérer les symboles non associatifs | herbelin |
| 2002-11-28 | Ajout d'une entre Prim.bigint | herbelin |
| 2002-11-26 | Réaffichage des Syntactic Definition (printer constr_expr). | herbelin |
