index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
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
*
Application des patches envoyés par F. Besson pour micromega
notin
2010-03-08
*
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
*
Improvements in generalized rewriting:
msozeau
2010-03-05
*
Add a generic tactic option builder. Use it in firstorder to set the
msozeau
2010-03-05
*
amelioration mineure dans Function
jforest
2010-03-01
*
Win32 cross-compilation from debian: build of coqide.exe and other binaries
letouzey
2010-02-24
*
correction of bug #2088
jforest
2010-02-24
*
Fix sort_dependencies for good, maintaining the initial order.
msozeau
2010-02-16
*
bug in field_simplify_eq in
barras
2010-02-10
*
Euclidean division for NArith
letouzey
2010-02-10
*
Fix [Existing Class] impl and add documentation. Fix computation of the
msozeau
2010-02-10
*
New command Declare Reduction <id> := <conv_expr>.
letouzey
2010-01-28
*
Backport fixes in Instance declarations to Program Instance.
msozeau
2010-01-28
*
Add [Next Obligation with tactic] support (wish #1953).
msozeau
2010-01-26
*
Fix bug #2086, error message when we match on an non-inductive type.
msozeau
2010-01-14
*
- Show Obligation Tactic
msozeau
2010-01-14
*
Support "Local Obligation Tactic" (now the default in sections).
msozeau
2010-01-11
*
Specific syntax for Instances in Module Type: Declare Instance
letouzey
2010-01-04
*
Few misc. updates.
herbelin
2010-01-04
*
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
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Const_omega: look for S in Init only (avoid future clash with S of Numbers)
letouzey
2009-12-18
*
correction de la nouvelle option pour functional induction
jforest
2009-12-16
*
adding an option functional_induction_rewrite_dependent to make functional in...
jforest
2009-12-16
*
Fixed incorrect computation of possible guard in presence of `{ ... } contexts.
herbelin
2009-12-12
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...
letouzey
2009-12-09
*
Fix the build of coq via ocamlbuild
letouzey
2009-12-08
*
Sos.ml: no more warnings
letouzey
2009-12-08
*
Continuing r12485-12486 and r12549 (cleaning around name generation)
herbelin
2009-12-02
*
Remove interface plugin
glondu
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
*
Fixing xml theory file export (was not consistent with coqdoc file
herbelin
2009-11-26
*
Module subtyping : allow many <: and module type declaration with <:
letouzey
2009-11-18
*
New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))
letouzey
2009-11-16
*
Oops, nf_evar_defs just changed to nf_evar_map.
msozeau
2009-11-12
*
Don't forget to normalize everything w.r.t. evars (fixes bug #2103).
msozeau
2009-11-12
*
Repair interpretation of numeral for BigQ, add a printer (close #2160)
letouzey
2009-11-12
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Added support for multiple where-clauses in Inductive and co (see wish #2163).
herbelin
2009-11-11
*
use only why-dp, support for z3
marche
2009-11-10
*
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
[next]