aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.mli
Commit message (Expand)AuthorAge
* 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
* DISCLAIMERGravatar puech2009-01-17
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* fixing problem with CompCert: reordering resulting from tac change was not cl...Gravatar barras2008-11-27
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* * Factorizing code : context_chop was used in several files (even as chop_con...Gravatar vsiles2008-03-17
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* - Ajout de la possibilité d'utiliser la notation Record pour lesGravatar herbelin2007-06-30
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Rework subtac pattern matching equalities generation.Gravatar msozeau2007-01-02
* Évitement des noms de constructeurs dans les motifs de filtrage de "match"Gravatar herbelin2006-12-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:30:03 +0000