aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
AgeCommit message (Expand)Author
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
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-02-17- Use transparency information all the way through unification andmsozeau
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-09-30Improve handling of metas as evars in unification (patch by Hugo)letouzey
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-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 08:00:34 +0000