| Commit message (Expand) | Author | Age |
... | |
* | A uniformization step around understand_* and interp_* functions. | herbelin | 2013-05-09 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of dir_path | ppedrot | 2012-12-14 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Implemented a full-fledged equality on [constr_expr]. By the way, | ppedrot | 2012-12-14 |
* | More equality functions | ppedrot | 2012-11-25 |
* | Taking into account the type of a definition (if it exists), and the | herbelin | 2012-11-17 |
* | Updating headers. | herbelin | 2012-08-08 |
* | 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-05-29 |
* | Added new command "Set Parsing Explicit" for deactivating parsing (and | herbelin | 2012-01-20 |
* | 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 | 2011-02-10 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
* | Added multiple implicit arguments rules per name. | herbelin | 2010-10-03 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | 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-07-22 |
* | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
* | 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-04-29 |
* | Backport fixes in Instance declarations to Program Instance. | msozeau | 2010-01-28 |
* | Promote evar_defs to evar_map (in Evd) | glondu | 2009-11-11 |
* | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin | 2009-11-11 |
* | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Use more consistent resolution parameters in Program and regular typing | msozeau | 2009-06-18 |
* | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
* | DISCLAIMER | puech | 2009-01-17 |
* | - Added support for subterm matching in SearchAbout. | herbelin | 2008-12-29 |
* | More factorization of inductive/record and typeclasses: move class | msozeau | 2008-11-09 |
* | Affichage des notations récursives: | herbelin | 2008-10-22 |
* | Add enough information to correctly globalize recursive calls in inductive and | msozeau | 2008-09-11 |
* | Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio... | notin | 2008-06-25 |
* | Improvements on coqdoc by adding more information into .glob | msozeau | 2008-05-30 |
* | Postpone the search for the recursive argument index from the user given | msozeau | 2008-05-06 |
* | Finish fix in command where we still lost information on what was a type | msozeau | 2008-03-24 |
* | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau | 2008-03-15 |
* | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |