aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
Commit message (Expand)AuthorAge
* 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
* 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
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* * Factorizing code : context_chop was used in several files (even as chop_con...Gravatar vsiles2008-03-17
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* 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
* Confusion sur le paramètre à donner à concrete_name lors du commit 9450Gravatar herbelin2006-12-14
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12