| Commit message (Expand) | Author | Age |
|---|
| * | [api] Misctypes removal: remove dummy alias. |  Emilio Jesus Gallego Arias | 2018-06-12 |
| * | [api] Misctypes removal: miscellaneous aliases. | Emilio Jesus Gallego Arias | 2018-06-12 |
| * | [api] Move universe syntax to `Glob_term` | Emilio Jesus Gallego Arias | 2018-05-08 |
| * | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. | Emilio Jesus Gallego Arias | 2018-05-04 |
| * | [api] Relocate `intf` modules according to dependency-order. | Emilio Jesus Gallego Arias | 2018-04-23 |
| * | Pattern as a mli-only file, operations in Patternops |  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-05-29 |
| * | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
| * | Glob_term.predicate_pattern: No number of parameters with letins. |  pboutill | 2012-03-02 |
| * | Noise for nothing | pboutill | 2012-03-02 |
| * | A pass on warning printings. Made systematic the use of msg_warning so |  herbelin | 2011-12-17 |
| * | Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors | letouzey | 2011-11-07 |
| * | Rename mkR* smart constructors (mostly in funind) |  glondu | 2010-12-25 |
| * | More {raw => glob} changes for consistency | glondu | 2010-12-24 |
| * | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
| * | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Fixed a bug introduced in a combination in r12807 and revealed in | herbelin | 2010-06-28 |
| * | Added support for Ltac-matching terms with variables bound in the pattern | herbelin | 2010-06-06 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | fixed confusion between number of cstr arguments and number of pattern variab... |  barras | 2010-03-12 |
| * | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
| * | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin | 2009-12-24 |
| * | First debug... the renaming of librairies was not working and auto/dn were no... |  soubiran | 2009-10-23 |
| * | This big commit addresses two problems: | soubiran | 2009-10-21 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Fix premature optimisation in dependent induction: even variable args need |  msozeau | 2009-04-10 |
| * | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
| * | Bugs, nettoyage, et améliorations diverses | herbelin | 2008-04-13 |
| * | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau | 2008-03-28 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
| * | Plus de combinateurs sont passés de Util à Option. Le module Options |  aspiwack | 2007-12-06 |
| * | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
| * | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
| * | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin | 2007-02-13 |
| * | bug serieux efficacite de ltac | barras | 2006-06-19 |
| * | - Distinction explicite des parties paramètres et arguments dans le type | herbelin | 2006-04-27 |
| * | Standardisation nom option_app en option_map | herbelin | 2006-04-27 |
| * | Timide tentative de clarification du statut de l'opérateur de filtrage | herbelin | 2006-04-24 |
| * | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
| * | Changement des named_context |  gregoire | 2005-12-02 |
| * | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin | 2005-11-08 |
| * | HUGE COMMIT |  sacerdot | 2005-01-03 |
| * | The type Pattern.constr_label was isomorphic to Libnames.global_reference. | sacerdot | 2004-12-07 |
| * | MAJ PCoFix | herbelin | 2004-11-26 |
| * | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot | 2004-11-16 |
| * | Nouvelle en-tête | herbelin | 2004-07-16 |
| * | Substitution dans REvar et PEvar plutot que encodage via noeud application po... | herbelin | 2003-12-19 |
Emilio Jesus Gallego Arias
letouzey
pboutill
herbelin
glondu
barras
soubiran
msozeau
aspiwack
gregoire
sacerdot