aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-21Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:msozeau
2012-06-20Fixing use of an error instead of a boolean result in the unificationherbelin
2012-06-15Reductionops : Better abstract machine stack utilitiespboutill
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
2012-03-22evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structuresgareuselesinge
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-02Noise for nothingpboutill
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
2011-11-08Refined second_order_matching so that a constraint on whichherbelin
2011-11-08optimization: memoization for is_open_canonical_projectiongareuselesinge
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-10-26Deactivating second-order pattern-matching in evarconv for 8.4.herbelin
2011-10-24Fixing instance/filter mismatch in materialize_evar + documentation.herbelin
2011-10-22Fail if some conv pbs remain after consider_remaining_unif_problems.herbelin
2011-10-22Use also second-order unification if first-order fails at the time of conside...herbelin
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
2011-10-10Applied the trick of Chung-Kil Hur to solve second-order matchingherbelin
2011-07-29Evarconv: generic equality on constr replaced by eq_constrpuech
2011-06-19Ensured that the transparency state is used when flag betaiota is on for apply.herbelin
2011-05-24Applying Enrico Tassi's patch for giving priority to delta over eta inherbelin
2011-03-31As remarked by Enrico, we'd better use eq_constr than structural equalityherbelin
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Revert commit r13883: instantiating ?n by a lambda when "?n a" has toherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-03-05Added support for instantiation of ?n by a lambda when "?n a" has toherbelin
2011-03-05Reorganized a bit evarconv.ml:herbelin
2011-02-17- Use transparency information all the way through unification andmsozeau
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-05-20Fix bug 2307pboutill
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-11Relatively ad hoc fix to an ill-typed instantiation bug in typeherbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-07-06change in the order of unification constraints solving (for canonical structu...amahboub
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 10:40:32 +0000