| Age | Commit message (Expand) | Author |
|---|
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | slim down a bit genarg.ml (pr_intro_pattern forgotten there) | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-20 | Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic | herbelin |
| 2012-03-18 | Fixing bug #2732 (anomaly when using the tolerance for writing | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Fix diagram in genarg.mli | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2009-12-24 | In "simpl c" and "change c with d", c can be a pattern. | herbelin |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-19 | Made the interpretation levels rlevel/glevel/tlevel truly phantom | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-06-07 | - Added two new introduction patterns with the following temptative syntaxes: | herbelin |
| 2008-10-19 | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin |
| 2008-10-11 | Backporting 11445 from 8.2 to trunk (negative conditions in | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-18 | Modification rapide du message d'erreur lorsqu'un _ ne peut être | herbelin |
| 2008-04-04 | Quelques améliorations des intro patterns: | herbelin |
| 2007-07-06 | New intro pattern "@A", which generates a fresh name based on A. | glondu |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 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-06-23 | documentation | herbelin |
| 2006-06-22 | Légère mise à jour | herbelin |
| 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-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-01-16 | Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom | herbelin |
| 2005-12-26 | Petite correction nom QuantHypArgType suite suppression traducteur | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-05-17 | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 2004-12-09 | Restauration type casted_open_constr pour tactique refine car l'unification n... | 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 |
| 2003-12-01 | Nouvelle tactique EExists | clrenard |
| 2003-11-17 | New tactics : econstructor, eleft, eright, esplit | clrenard |
| 2003-05-21 | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin |
