aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-19Fixing bug #2454: inversion predicate strategy for inferring the typeherbelin
2010-10-06Fixing the Not_found error in bug #2404 + dead code removal in cases.mlherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-12Improved the inference of the return predicate in dependent pattern-matching.herbelin
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
2010-06-10Fixed two bugs in pattern-matching compilationherbelin
2010-05-20Fix bug 2307pboutill
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
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