| Age | Commit message (Expand) | Author |
|---|
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | 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-01-20 | Added new command "Set Parsing Explicit" for deactivating parsing (and | herbelin |
| 2011-02-10 | Interp a definition with the implicit arguments of its local context | pboutill |
| 2011-02-10 | local variables can have implicits locally | pboutill |
| 2011-02-10 | Data structure telling implicits of local variables is a map in the | pboutill |
| 2011-02-10 | More comments and less doublons in some mli | pboutill |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-10-03 | Added multiple implicit arguments rules per name. | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-22 | Extension of the recursive notations mechanism | herbelin |
| 2010-07-22 | Simplified the way internalization_data (i.e. bindings of bound vars | herbelin |
| 2010-07-22 | Constrintern: unified push_name_env and push_loc_name_env; made | herbelin |
| 2010-07-22 | Switch to American spelling for "internalise" and "internalisation" | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Various minor improvements of comments in mli for ocamldoc | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-01-28 | Backport fixes in Instance declarations to Program Instance. | msozeau |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-11-11 | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-18 | Use more consistent resolution parameters in Program and regular typing | msozeau |
| 2009-03-28 | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau |
| 2009-01-17 | DISCLAIMER | puech |
| 2008-12-29 | - Added support for subterm matching in SearchAbout. | herbelin |
| 2008-11-09 | More factorization of inductive/record and typeclasses: move class | msozeau |
| 2008-10-22 | Affichage des notations récursives: | herbelin |
| 2008-09-11 | Add enough information to correctly globalize recursive calls in inductive and | msozeau |
| 2008-06-25 | Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio... | notin |
| 2008-05-30 | Improvements on coqdoc by adding more information into .glob | msozeau |
| 2008-05-06 | Postpone the search for the recursive argument index from the user given | msozeau |
| 2008-03-24 | Finish fix in command where we still lost information on what was a type | msozeau |
| 2008-03-15 | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-07-02 | Fix bug in subst_cases_pattern when aliasing recursive notations. | msozeau |
| 2007-05-06 | Nouveaux changements autour des implicites (notamment suite à | herbelin |
| 2007-04-29 | Multiples changements autour des implicites : | herbelin |
| 2007-03-28 | Support for implicit formal argument types in Program ; parse types in type s... | msozeau |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2006-09-20 | Declarative Proof Language: main commit | corbinea |
| 2006-09-01 | Export de fonctions d'interprétation acceptant des evars non résolues | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-21 | Restructuration des points d'entrée de Pretyping et Constrintern | herbelin |
| 2005-09-09 | Conséquences nettoyage pretyping.ml | herbelin |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
