aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/genarg.mli
Commit message (Expand)AuthorAge
* Modulification of identifierGravatar ppedrot2012-12-14
* More equality functionsGravatar ppedrot2012-11-25
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* slim down a bit genarg.ml (pr_intro_pattern forgotten there)Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Noise for nothingGravatar pboutill2012-03-02
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Fix diagram in genarg.mliGravatar glondu2010-12-23
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Made the interpretation levels rlevel/glevel/tlevel truly phantomGravatar herbelin2009-12-19
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* 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
* documentationGravatar herbelin2006-06-23
* Légère mise à jourGravatar herbelin2006-06-22
* 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
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomGravatar herbelin2006-01-16
* Petite correction nom QuantHypArgType suite suppression traducteurGravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* 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