aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
Commit message (Expand)AuthorAge
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
* Partial application hunt.Gravatar ppedrot2013-11-07
* Closure optimizations.Gravatar ppedrot2013-10-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Array.create is deprecatedGravatar pboutill2012-12-19
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
* Small cleaning of interface in UnivGravatar ppedrot2012-11-26
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Added a CString module.Gravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* More cleaning in CArray...Gravatar ppedrot2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Reorganizing Unification.unify_0 so as to more easily share codeGravatar herbelin2011-12-17
* Backtrack on synchronizing universe counter with resetGravatar herbelin2011-12-06
* Registering universe and meta/evar counters as summaries so as toGravatar herbelin2011-12-05
* Fixed a small regression in pattern-matching compilation introduced inGravatar herbelin2011-12-04
* Fixing buggy abberant code for Evarutil.expand_evarGravatar herbelin2011-10-10
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* Generalizing subst_term_occ so that it supports an arbitrary matchingGravatar herbelin2011-09-26
* Adding subst_term up to convGravatar herbelin2011-09-26
* Added full pattern-unification on Meta for tactic unification.Gravatar herbelin2011-06-13
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24