index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
subtac
Commit message (
Expand
)
Author
Age
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Replaced printing number of ill-typed branch by printing name of constructor
herbelin
2011-04-08
*
Extraction: unfolds the let-in created by Program when handling "match"
letouzey
2011-04-07
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Keep information on which fields are subclasses in class declarations,
msozeau
2011-03-11
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
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
*
Improved define_evar_as_lambda which was creating an unrelated new evar
herbelin
2011-03-05
*
Add a flag to hide obligations in Program-generated terms under an
msozeau
2011-02-28
*
Interp a definition with the implicit arguments of its local context
pboutill
2011-02-10
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Remove an unused function with a Evd.fold in subtac
letouzey
2010-12-13
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Add information of localisation when an error involving an "implicit
herbelin
2010-11-07
*
Cleaning the use of parentheses around evd and evdref (cosmetic commit).
herbelin
2010-10-31
*
Fix bug #2393: allow let-ins inside telescopes (only fails when there's
msozeau
2010-10-12
*
Fix bug# 2392
msozeau
2010-10-07
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Fix bug #2321, allowing "_" named projections in classes. Not realizing
msozeau
2010-09-28
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Minor fixes:
msozeau
2010-07-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Simplified the way internalization_data (i.e. bindings of bound vars
herbelin
2010-07-22
*
Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).
herbelin
2010-07-22
*
Move [delayed] to util and use [force_delayed] everywhere to force
msozeau
2010-06-30
*
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
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Fix bug #2262: bad implicit argument number by avoiding counting
msozeau
2010-06-09
*
Fix treatment of {struct x} annotations in presence of generalized
msozeau
2010-06-08
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
static (and shared) camlp4use instead of per-file declaration
letouzey
2010-05-19
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
*
Oops, don't use zeta by default.
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
*
Consider OccurCheck a catchable exception.
msozeau
2010-03-08
[next]