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