aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* 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
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Improve return predicate inference by making the return type dependentGravatar msozeau2009-06-28
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Fix (?) a pattern matching compilation problem: Gravatar msozeau2008-11-27
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Finish enhancemenent of return clause inference from tycons, integratingGravatar msozeau2008-04-01
* Fix test-suite files, change conflicting notation "->rel" and the othersGravatar msozeau2008-03-29
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.Gravatar herbelin2007-09-25
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* - Correction d'un bug de de Bruijn dans abstract_predicate (lié auGravatar herbelin2007-08-10
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Code mort découvert par MatthieuGravatar herbelin2006-11-22
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* Correction d'un bug de coercion de pattern introduit dans la 8.1betaGravatar herbelin2006-09-23
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Typo dans précédent commit (8755); protection renforcée dans analyse claus...Gravatar herbelin2006-04-28
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Code mort (suite)Gravatar herbelin2006-04-25
* Suppression code mortGravatar herbelin2006-04-25
* Pas fierGravatar herbelin2006-04-14
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...Gravatar msozeau2006-04-10
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Suppression fonctions d'interprétation du vieux CaseGravatar herbelin2006-01-30
* - Prise en compte de la clause 'in I' pour coercer le type du terme à filtrerGravatar herbelin2006-01-30
* - Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;Gravatar herbelin2006-01-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* pas besoin de List.length pour savoir si une liste est videGravatar letouzey2005-08-19
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* evar declarees avec mauvais typeGravatar barras2005-06-08