aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2009-12-30Fixing bug #2193: computation of dependencies in the "match" returnherbelin
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-28Improve return predicate inference by making the return type dependentmsozeau
2009-06-06Fixing bug #2106 ("match" compilation with multi-dependent constructor).herbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-06pushed evar reduction in kernelbarras
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-11-27Fix (?) a pattern matching compilation problem: msozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-10- Correction bug 1841 (identificateurs incorrects avec Subclass)herbelin
2008-06-09- Correction de la version simplifiée (filtrage sur deux sigherbelin
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-04-01Finish enhancemenent of return clause inference from tycons, integratingmsozeau
2008-03-29Fix test-suite files, change conflicting notation "->rel" and the othersmsozeau
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-09-25Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.herbelin
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
2007-08-10- Correction d'un bug de de Bruijn dans abstract_predicate (lié auherbelin
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2006-11-22Code mort découvert par Matthieuherbelin
2006-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
2006-09-23Correction d'un bug de coercion de pattern introduit dans la 8.1betaherbelin
2006-05-29The "clean integration of subtac" patch.msozeau
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-04-28Typo dans précédent commit (8755); protection renforcée dans analyse claus...herbelin
2006-04-27- Distinction explicite des parties paramètres et arguments dans le typeherbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-25Code mort (suite)herbelin
2006-04-25Suppression code mortherbelin
2006-04-14Pas fierherbelin
2006-04-10Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...msozeau
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-01-30Suppression fonctions d'interprétation du vieux Caseherbelin
2006-01-30- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrerherbelin
2006-01-30- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin