aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Printing bugs with match patterns:Gravatar herbelin2012-01-27
* Fix for Program Instance not separately checking the resolution of evars of t...Gravatar msozeau2012-01-23
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
* Type inference unification: fixed a 8.4 bug in the presence of unificationGravatar herbelin2012-01-04
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
* Continuing 14812 and 14813 (use type information to reduce theGravatar herbelin2011-12-18
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
* Added ability to take the type of applied metas into account whenGravatar herbelin2011-12-17
* Reorganizing Unification.unify_0 so as to more easily share codeGravatar herbelin2011-12-17
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
* Fixing a bug of commit r13310 (activating coercions only when moduleGravatar herbelin2011-12-07
* Backtrack on synchronizing universe counter with resetGravatar herbelin2011-12-06
* Registering universe and meta/evar counters as summaries so as toGravatar herbelin2011-12-05
* Yet another fix about alias in testing if pattern unification applies.Gravatar herbelin2011-12-05
* Fixed a small regression in pattern-matching compilation introduced inGravatar herbelin2011-12-04
* Discarding let-ins from the instances of the evars in theGravatar herbelin2011-12-04
* Finally used typing to decide whether an alias needs to be expanded orGravatar herbelin2011-11-28
* Fixing dependencies postprocessing bug in pattern-matching compilation.Gravatar herbelin2011-11-28
* Fixed a bug in postprocessing dependencies in pattern-matching compilationGravatar herbelin2011-11-26
* avoid relying on weak invariant in cbv.mlGravatar bgregoir2011-11-25
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Adds a pair of function in Evar_util to gather dependent evars in anGravatar aspiwack2011-11-23
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* Configurable simpl tacticGravatar gareuselesinge2011-11-21
* Extend the computation of dependencies in pattern-matching compilationGravatar herbelin2011-11-21
* Add matching on non-inductive types in building an inversion problemGravatar herbelin2011-11-21
* Old naming bug in pattern-matching compilation: names in theGravatar herbelin2011-11-21
* Inlining let-in (i.e. trace of aliases) in extract_predicate for whatGravatar herbelin2011-11-21
* In pattern-matching compilation, now taking into account the dependenciesGravatar herbelin2011-11-21
* Optimizing the compilation of unused aliases in pattern-matching.Gravatar herbelin2011-11-21
* Simplifying history management in pattern-matching compilation.Gravatar herbelin2011-11-21
* Fixing postprocessing bugs in pattern-matching compilation.Gravatar herbelin2011-11-21
* Removing stuff about alias dependencies now become useless.Gravatar herbelin2011-11-21
* Changed the way to detect if an "as" patterns is expanded or not. TheGravatar herbelin2011-11-21
* Dead code + refreshing some comments in cases.ml.Gravatar herbelin2011-11-21
* Restore backward compatibility. ":>" declares subinstances in Class declarati...Gravatar msozeau2011-11-18
* Fix for subclasses implementation, allowing to register generalized classes s...Gravatar msozeau2011-11-18
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-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
* Refined second_order_matching so that a constraint on whichGravatar herbelin2011-11-08