aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
2012-06-15Reductionops : Better abstract machine stack utilitiespboutill
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
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-20Fix interface of resolve_typeclasses: onlyargs -> with_goals: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-02Noise for nothingpboutill
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-04Discarding let-ins from the instances of the evars in theherbelin
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-16A bit of documentation around cases.ml + ML modules uselessly openherbelin
2011-11-08Refined second_order_matching so that a constraint on whichherbelin
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-06-20Fixing two typos introduced in r14217 and r14223herbelin
2011-06-19Ensured that the transparency state is used when flag betaiota is on for apply.herbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-18Activating flags betaiota by default for applyherbelin
2011-06-18The ad hoc version for first-order unification at toplevel of "?n argsherbelin
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-12Oups, typo in previous commitherbelin
2011-06-12Removed what looks like a (very old) useless f.o. unification passherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-05-05Fix merge, Cumul moved to CUMULmsozeau
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
2011-04-20Allow betaiota when checking unification of the types of metas (fixes ATBR co...msozeau
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-04-16Fix unification of types of metavariables and error message for sort unificat...msozeau
2011-04-13- Remove create_evar_defsmsozeau
2011-04-13- Improve unification (beta-reduction, and same heuristic as evarconv for red...msozeau
2011-04-13Unify meta types with the right flags, add betaiotazeta reduction to unificat...msozeau
2011-04-13Proper typing of metavariables, type errors were completely ignored before......msozeau
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-08Solve evar instantiations in the right environment.msozeau
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:32:48 +0000