aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.mli
Commit message (Expand)AuthorAge
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Extra check for indirect dependency when abstracting a term which isGravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
* 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
* comments in mliGravatar pboutill2013-05-30
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Comments in mliGravatar pboutill2013-03-25
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Updating headers.Gravatar herbelin2012-08-08
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* 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
* 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
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Added rudimentary support for using constructors from the explicitGravatar herbelin2010-06-12
* Fix bug 2307Gravatar pboutill2010-05-20
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Compromise wrt introduction-names compatibility issue after additionGravatar herbelin2009-03-22