aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-12-04Fixed a small regression in pattern-matching compilation introduced inherbelin
2011-11-28Finally used typing to decide whether an alias needs to be expanded orherbelin
2011-11-28Fixing dependencies postprocessing bug in pattern-matching compilation.herbelin
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-21Add matching on non-inductive types in building an inversion problemherbelin
2011-11-21Old naming bug in pattern-matching compilation: names in theherbelin
2011-11-21Inlining let-in (i.e. trace of aliases) in extract_predicate for whatherbelin
2011-11-21In pattern-matching compilation, now taking into account the dependenciesherbelin
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
2011-11-21Simplifying history management in pattern-matching compilation.herbelin
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
2011-11-21Removing stuff about alias dependencies now become useless.herbelin
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
2011-11-21Dead code + refreshing some comments in cases.ml.herbelin
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
2011-11-16Adding postprocessing to remove "commutative cuts" expansions inherbelin
2011-11-16Changed the way find_dependencies_signature is working so that itherbelin
2011-11-16De Bruijn indices bug in pattern matching compilation in the presenceherbelin
2011-11-16Old generalization bug in pattern-matching: names were considered theherbelin
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
2011-11-16Old typing bug in pattern-matching compilation (apparently w/oherbelin
2011-11-16Specialization of tomatch in pattern-matching compilation was done tooherbelin
2011-11-16A bit of documentation around cases.ml + ML modules uselessly openherbelin
2011-11-16Fixing dependencies lifting bug in pattern-matching compilationherbelin
2011-10-25Fixing use of type constraint for refining the "return" clause of "match".herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-08-08Two bugs in pattern-matching compilation:herbelin
2011-07-29Cases: generic equality on constr replaced by destructorspuech
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2010-12-24More {raw => glob} changes for consistencyglondu
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