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
...
*
Fix treatment of remaining unification constraints: raise a more
msozeau
2010-03-07
*
Add a generic tactic option builder. Use it in firstorder to set the
msozeau
2010-03-05
*
Fix sort_dependencies for good, maintaining the initial order.
msozeau
2010-02-16
*
Fix [Existing Class] impl and add documentation. Fix computation of the
msozeau
2010-02-10
*
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
*
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
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
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
*
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
*
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
*
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
*
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
*
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
*
- Resolve type class constraints before trying to find unresolved
msozeau
2009-09-11
*
Misc fixes:
msozeau
2009-09-10
*
Hack to correctly get ill-formed rec body exceptions even
msozeau
2009-09-02
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Fix bug introduced by last revision, subtac_cases was returning the
msozeau
2009-06-29
*
Abstract the tycon by the matched terms when turning them into variables
msozeau
2009-06-28
*
Improve return predicate inference by making the return type dependent
msozeau
2009-06-28
*
Fixes for r12197, the refined evars were not returned in case fail_evar
msozeau
2009-06-22
*
Use more consistent resolution parameters in Program and regular typing
msozeau
2009-06-18
*
Fallback on not using [fix_proto] if the right imports aren't there, the
msozeau
2009-06-17
*
Use a lazy value for the message in FailError, so that it won't be
msozeau
2009-06-11
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Fix de Bruijn lifting bug appearing when we match on multiple terms with
msozeau
2009-05-26
*
Support for definition hooks in subtac.
msozeau
2009-05-16
*
More efficient handling of evars in Program Fixpoint commands.
msozeau
2009-04-28
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
- New cleaning phase for the entry points of pretyping.ml
herbelin
2009-04-24
*
Better Requires in Classes. Fix bug #2093: the code does not require
msozeau
2009-04-16
[prev]
[next]