aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
Commit message (Expand)AuthorAge
* 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
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* Added rudimentary support for using constructors from the explicitGravatar herbelin2010-06-12
* Fix bug 2307Gravatar pboutill2010-05-20
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-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
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* 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
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* - 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
* * Fixed constr_cmp again to handle universes subtyping correctlyGravatar puech2008-10-09
* Fixing constr_cmp, propagating subtyping only right of a productGravatar puech2008-10-02
* Fix a bug, in fold_constr_with_binders, the types of fixpoints wereGravatar msozeau2008-09-13
* Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parGravatar herbelin2008-08-04
* Backport r11289.Gravatar msozeau2008-07-29
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:37:39 +0000