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
*
Made coercions active only when modules are imported.
herbelin
2010-07-22
*
Reverted 13293 commited mistakenly. Sorry for the noise.
herbelin
2010-07-18
*
Tentative de suppression de l'import automatique des hints et coercions.
herbelin
2010-07-18
*
Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.
msozeau
2010-06-30
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Fixed a bug introduced in a combination in r12807 and revealed in
herbelin
2010-06-28
*
Applying François' patches about Canonical Projections (see #2302 and #2334).
herbelin
2010-06-26
*
Restored a "feature" of unification in pre-8.3 (it was used e.g. in a
herbelin
2010-06-25
*
Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).
herbelin
2010-06-22
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).
herbelin
2010-06-18
*
Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"
herbelin
2010-06-13
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Improved the inference of the return predicate in dependent pattern-matching.
herbelin
2010-06-12
*
Added rudimentary support for using constructors from the explicit
herbelin
2010-06-12
*
Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).
herbelin
2010-06-12
*
Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).
herbelin
2010-06-11
*
Fixed two bugs in pattern-matching compilation
herbelin
2010-06-10
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Documentation of pretype_id (minor commit).
herbelin
2010-05-28
*
Fixing Derive Inversion for new proof engine
herbelin
2010-05-26
*
Fix bug 2307
pboutill
2010-05-20
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Some ocamldoc comments + Fixing name of .coqrc.version file in refman
pboutill
2010-05-18
*
Applicative commutative cuts in Fixpoint guard condition
pboutill
2010-05-18
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Deux commentaires retirés de ocamldoc.
aspiwack
2010-05-07
*
ocamldoc related fixes
pboutill
2010-05-03
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Misc small fixes : warning, dep cycles, ocamlbuild...
letouzey
2010-04-26
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Fixed bugs from commit 12954 on unification complexity
herbelin
2010-04-20
*
Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).
herbelin
2010-04-19
*
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
[next]