index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
unification.ml
Commit message (
Expand
)
Author
Age
*
A bit of documentation around cases.ml + ML modules uselessly open
herbelin
2011-11-16
*
Refined second_order_matching so that a constraint on which
herbelin
2011-11-08
*
Improved check is_open_canonical_projection
gareuselesinge
2011-11-08
*
Fixing incorrect change to pattern-unification over Meta's introduced
herbelin
2011-11-06
*
Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed
herbelin
2011-10-11
*
Moved to a more standard order of arguments (i.e. env followed by evar_map)
herbelin
2011-10-11
*
More robust and uniform treatment of aliases in evarutil.ml
herbelin
2011-10-10
*
Generalizing subst_term_occ so that it supports an arbitrary matching
herbelin
2011-09-26
*
Propagated information from the reduction tactics to the kernel so
herbelin
2011-08-10
*
Fix unification: detect invalid evar instantiations due to scoping earlier.
msozeau
2011-08-04
*
Fixing two typos introduced in r14217 and r14223
herbelin
2011-06-20
*
Ensured that the transparency state is used when flag betaiota is on for apply.
herbelin
2011-06-19
*
Generalizing flag use_evars_pattern_unification into a flag
herbelin
2011-06-18
*
Activating flags betaiota by default for apply
herbelin
2011-06-18
*
The ad hoc version for first-order unification at toplevel of "?n args
herbelin
2011-06-18
*
Added full pattern-unification on Meta for tactic unification.
herbelin
2011-06-13
*
Added a flag to restrict conversion in tactic unification on the
herbelin
2011-06-13
*
Oups, typo in previous commit
herbelin
2011-06-12
*
Removed what looks like a (very old) useless f.o. unification pass
herbelin
2011-06-12
*
Added a new flag for freezing evars in tactic unification. Used this
herbelin
2011-06-12
*
Moved allow_K to a unification flag
herbelin
2011-06-10
*
Fix merge, Cumul moved to CUMUL
msozeau
2011-05-05
*
Merge branch 'subclasses' into coq-trunk
msozeau
2011-05-05
*
First phase removing obsolete support for eta up to conversion in
herbelin
2011-05-04
*
Allow betaiota when checking unification of the types of metas (fixes ATBR co...
msozeau
2011-04-20
*
Add a flag to control betaiota reduction during unification to maintain backw...
msozeau
2011-04-18
*
Fix unification of types of metavariables and error message for sort unificat...
msozeau
2011-04-16
*
- Remove create_evar_defs
msozeau
2011-04-13
*
- Improve unification (beta-reduction, and same heuristic as evarconv for red...
msozeau
2011-04-13
*
Unify meta types with the right flags, add betaiotazeta reduction to unificat...
msozeau
2011-04-13
*
Proper typing of metavariables, type errors were completely ignored before......
msozeau
2011-04-13
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Solve evar instantiations in the right environment.
msozeau
2011-03-08
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
*
- Use transparency information all the way through unification and
msozeau
2011-02-17
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Improve handling of metas as evars in unification (patch by Hugo)
letouzey
2010-09-30
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Restored a "feature" of unification in pre-8.3 (it was used e.g. in a
herbelin
2010-06-25
*
Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).
herbelin
2010-06-18
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").
herbelin
2010-04-11
*
Added a function in typing.ml to solve evars of a constr w/o going back down ...
herbelin
2010-04-05
*
Granting wish #2251 (forbidding rewriting a term reduced to an evar)
herbelin
2010-04-05
[next]