aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2012-05-11Impossible branches inference fixup (bug 2761)pboutill
2012-04-27Partial revert of r15148 in order to compile with Camlp4pboutill
2012-04-25Avoid unneeded head-normalizations in coercion code.msozeau
2012-04-25Do not delta-head-normalize the proposition argument of sigma types during co...msozeau
2012-04-18Corrects a bug in the refine tactic which could drop evar bodies.aspiwack
2012-04-18Adds a comment: precondition on Evd.addaspiwack
2012-04-16Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.herbelin
2012-04-05Speedup free_vars_and_rels_up_alias_expansion (evarconv)gareuselesinge
2012-03-26Unification: Fixing bug in materialize_evar (spotted by MathClasses).herbelin
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
2012-03-23Little bug in r15061 leading to unusable debug mode.herbelin
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-22evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structuresgareuselesinge
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-20Use a careful analysis of dependencies in restricting instances toherbelin
2012-03-20Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep aherbelin
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
2012-03-20Reorganizing the structure of evarutil.ml (only restructuration, noherbelin
2012-03-19More adaptations of pretyping/coercion to Program mode.msozeau
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-19Fixes bug: #2692 (Arguments/simpl off by 1)gareuselesinge
2012-03-19Arguments/simpl: allow ! even on non fixpointsgareuselesinge
2012-03-14Fix merge and add missing file.msozeau
2012-03-14Revise API of understand_ltac to be parameterized by a flag for resolution of...msozeau
2012-03-14Merge fixesmsozeau
2012-03-14Everything compiles again.msozeau
2012-03-14Second step of integration of Program:msozeau
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-03-13A bit of cleaning: unifying push_rels and push_rel_context.herbelin
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-03-02Noise for nothingpboutill
2012-03-01Univ: a univ_depends function to avoid a hack in Inductiveopsletouzey
2012-02-15Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...msozeau
2012-01-31Bug #2041: unfold at betaiotaZETA normalize like unfoldpboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2012-01-27Printing bugs with match patterns:herbelin
2012-01-23Fix for Program Instance not separately checking the resolution of evars of t...msozeau
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-12-18Continuing 14812 and 14813 (use type information to reduce theherbelin
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-12-17Added ability to take the type of applied metas into account whenherbelin
2011-12-17Reorganizing Unification.unify_0 so as to more easily share codeherbelin
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 00:43:57 +0000