index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
Commit message (
Expand
)
Author
Age
...
*
Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml
letouzey
2012-05-29
*
correct abort in Function when a proof of inversion fails
letouzey
2012-04-23
*
"A -> B" is a notation for "forall _ : A, B".
pboutill
2012-04-12
*
info_trivial, info_auto, info_eauto, and debug (trivial|auto)
letouzey
2012-03-30
*
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
Fixing bug #2732 (anomaly when using the tolerance for writing
herbelin
2012-03-18
*
Final part of moving Program code inside the main code. Adapted add_definitio...
msozeau
2012-03-14
*
Second step of integration of Program:
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
New version of recdef :
jforest
2012-03-01
*
various corrections in invfun due to a modification in induction
jforest
2012-03-01
*
correcting a little bug in invfun.ml
jforest
2012-02-29
*
correction of bug 2457
jforest
2012-02-29
*
In the syntax of pattern matching, "in" clauses are patterns.
pboutill
2012-02-29
*
correcting inversion in list of generated tcc of Function
letouzey
2012-02-03
*
Proof using ...
gareuselesinge
2011-12-12
*
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-24
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Remove avoidable use of GDynamic
glondu
2011-10-27
*
Fixing Equality.injectable which did not detect an equality without
herbelin
2011-10-22
*
Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).
herbelin
2011-10-05
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
correction du bug 2047
jforest
2011-09-09
*
Recdef: replaced some generic = on constr by eq_constr
puech
2011-07-29
*
Functional_principles_types: replaced some generic = on constr by eq_constr
puech
2011-07-29
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
Call process_vernac_interp_error before calling Errors.print in
herbelin
2011-06-10
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED
glondu
2010-12-25
*
Rename mkR* smart constructors (mostly in funind)
glondu
2010-12-25
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename files in funind to respect new conventions
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
*
Prepare change of nomenclature rawconstr -> glob_constr
glondu
2010-12-23
*
An experimental support for open constrs in hints and in "using"
herbelin
2010-10-31
*
Auto-inlining of f_terminate in Function
jforest
2010-10-05
*
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-09-30
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Remove "init" label from Termops.it_mk* specialized functions
glondu
2010-09-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Report fix bug 2345 from v8.3 (Bad error message when functional
courtieu
2010-09-21
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
[prev]
[next]