aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Speedup free_vars_and_rels_up_alias_expansion (evarconv)Gravatar gareuselesinge2012-04-05
* Unification: Fixing bug in materialize_evar (spotted by MathClasses).Gravatar herbelin2012-03-26
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
* Little bug in r15061 leading to unusable debug mode.Gravatar herbelin2012-03-23
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
* evarconv: MaybeFlex/MaybeFlex case infers more Canonical StructuresGravatar gareuselesinge2012-03-22
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Use a careful analysis of dependencies in restricting instances toGravatar herbelin2012-03-20
* Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep aGravatar herbelin2012-03-20
* Generalized the use of evar candidates in type inference unification:Gravatar herbelin2012-03-20
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
* More adaptations of pretyping/coercion to Program mode.Gravatar msozeau2012-03-19
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Fixes bug: #2692 (Arguments/simpl off by 1)Gravatar gareuselesinge2012-03-19
* Arguments/simpl: allow ! even on non fixpointsGravatar gareuselesinge2012-03-19
* Fix merge and add missing file.Gravatar msozeau2012-03-14
* Revise API of understand_ltac to be parameterized by a flag for resolution of...Gravatar msozeau2012-03-14
* Merge fixesGravatar msozeau2012-03-14
* Everything compiles again.Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* A bit of cleaning: unifying push_rels and push_rel_context.Gravatar herbelin2012-03-13
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
* Noise for nothingGravatar pboutill2012-03-02
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
* Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...Gravatar msozeau2012-02-15
* Bug #2041: unfold at betaiotaZETA normalize like unfoldGravatar pboutill2012-01-31
* Added an pattern / occurence syntax for vm_compute.Gravatar ppedrot2012-01-30
* 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