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
*
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
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
OrderedType implementation for various numerical datatypes + min/max structures
letouzey
2009-11-03
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Make usage of Dyn explicit
glondu
2009-10-28
*
Add a new vernacular command for controling implicit generalization of
msozeau
2009-10-27
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Fix bug #2162 and a name clashing bug in generalized binders.
msozeau
2009-10-09
*
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-10-08
*
Fix for missing hypotesae in XML proof tree export.
cek
2009-10-07
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Fixed small name freshness bug in Functional Scheme ("Heq" name was
herbelin
2009-10-03
*
Add support for Local Declare ML Module
glondu
2009-09-29
*
Fix the stdlib doc compilation + switch all .v file to utf8
letouzey
2009-09-28
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
micromega: better handling of exponentiation + correction of test-suite termi...
fbesson
2009-09-18
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Dont't forget to update the state or an obligation tactic assignment may
msozeau
2009-09-15
*
Stop using [obligation_tactic] from Program.Tactics as the default
msozeau
2009-09-15
*
Backtrack on the forced discharge of type class variables introduced
msozeau
2009-09-14
*
- Inductive types in the "using" option of auto/eauto/firstorder are
herbelin
2009-09-13
[next]