index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
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
*
Partial fix to bug #2244 (ensure that pattern unification does not
herbelin
2010-04-05
*
Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphic
herbelin
2010-03-28
*
Fixing bug #2279 (printing nested let-in was in exponential time)
herbelin
2010-03-27
*
Stop dropping evar constraints when building a new goal evar defs.
msozeau
2010-03-15
*
Fix splitting evars tactics and stop dropping evar constraints when
msozeau
2010-03-15
*
fixed confusion between number of cstr arguments and number of pattern variab...
barras
2010-03-12
*
fix [Search] when the result has no hypothesis & constant comparison
puech
2010-03-11
*
Reorder resolution of type class and unification constraints.
msozeau
2010-03-07
*
Fix treatment of remaining unification constraints: raise a more
msozeau
2010-03-07
*
Improve unification when evars and metas are mixed.
msozeau
2010-02-22
*
Compute the correct generalization information when discharging a class
msozeau
2010-02-16
*
Fix [Existing Class] impl and add documentation. Fix computation of the
msozeau
2010-02-10
*
Quick fix for references to section variables unbound in the current
msozeau
2010-01-26
*
Removing some betaiota-redexes in error messages (an experiment)
herbelin
2010-01-12
*
Typo in error message
herbelin
2010-01-12
*
Added module sharing support for typeclasses and hints (pri_auto_tactic).
soubiran
2010-01-12
*
Fix handling of instance declarations in presence of let-ins (bug
msozeau
2010-01-01
*
Fixing bug #2193: computation of dependencies in the "match" return
herbelin
2009-12-30
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Opened the possibility to type Ltac patterns but it is not fully functional yet
herbelin
2009-12-24
*
Attached evar source to the evar_info and add location to tclWITHHOLES errors
herbelin
2009-12-22
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
In "progress", extending the set of evars w/o solving an existing one is
herbelin
2009-12-21
*
Improved strategy for rewriting lemma possibly depending because of evars.
herbelin
2009-12-14
*
Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)
herbelin
2009-12-03
*
Continuing r12485-12486 and r12549 (cleaning around name generation)
herbelin
2009-12-02
*
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-12-01
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Fix type class discharge again.
msozeau
2009-11-15
*
Backtrack on fixing #2167
herbelin
2009-11-12
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Redoing broken commit r12498 (fixing bug #2167 + attempt to test the
herbelin
2009-11-11
*
Fixing bug #2167 + attempt to test the compatibility of a more robust
herbelin
2009-11-11
*
Commit 12485 continued.
herbelin
2009-11-09
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Took local definitions into account in the test for deciding whether
herbelin
2009-11-08
*
- Fix discharge bug in typeclasses: some constrs were not actually
msozeau
2009-11-06
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
Reverted an incorrect code simplification in function status_changed
herbelin
2009-11-02
*
Attempt to capture on time unification errors for "with" bindings.
herbelin
2009-10-30
*
Take constraints into account in the "instantiate" tactic
herbelin
2009-10-30
*
Fix bug in dnet.ml, which missed some results when filtering one term against...
puech
2009-10-29
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Remove old compatibility stuff (Tacred.nf)
glondu
2009-10-28
*
Make usage of Dyn explicit
glondu
2009-10-28
*
Fixes around typeclasses:
msozeau
2009-10-27
[next]