aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
...
* Dead code + refreshing some comments in cases.ml.Gravatar herbelin2011-11-21
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
* Adding postprocessing to remove "commutative cuts" expansions inGravatar herbelin2011-11-16
* Changed the way find_dependencies_signature is working so that itGravatar herbelin2011-11-16
* De Bruijn indices bug in pattern matching compilation in the presenceGravatar herbelin2011-11-16
* Old generalization bug in pattern-matching: names were considered theGravatar herbelin2011-11-16
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
* Old typing bug in pattern-matching compilation (apparently w/oGravatar herbelin2011-11-16
* Specialization of tomatch in pattern-matching compilation was done tooGravatar herbelin2011-11-16
* A bit of documentation around cases.ml + ML modules uselessly openGravatar herbelin2011-11-16
* Fixing dependencies lifting bug in pattern-matching compilationGravatar herbelin2011-11-16
* Fixing use of type constraint for refining the "return" clause of "match".Gravatar herbelin2011-10-25
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Two bugs in pattern-matching compilation:Gravatar herbelin2011-08-08
* Cases: generic equality on constr replaced by destructorsGravatar puech2011-07-29
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Fixing the Not_found error in bug #2404 + dead code removal in cases.mlGravatar herbelin2010-10-06
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Improved the inference of the return predicate in dependent pattern-matching.Gravatar herbelin2010-06-12
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
* Fixed two bugs in pattern-matching compilationGravatar herbelin2010-06-10
* Fix bug 2307Gravatar pboutill2010-05-20
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixing bug #2193: computation of dependencies in the "match" returnGravatar herbelin2009-12-30
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 14:35:34 +0000