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
*
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
*
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
[next]