index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
...
*
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
*
Attached evar source to the evar_info and add location to tclWITHHOLES errors
herbelin
2009-12-22
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
In "progress", extending the set of evars w/o solving an existing one is
herbelin
2009-12-21
*
Made the interpretation levels rlevel/glevel/tlevel truly phantom
herbelin
2009-12-19
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Promote evar_defs to evar_map (in Evd)
glondu
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
*
Take constraints into account in the "instantiate" tactic
herbelin
2009-10-30
*
Remove old compatibility stuff (Tacred.nf)
glondu
2009-10-28
*
fixed czar bug with parametric inductives
corbinea
2009-10-27
*
Add support for remaining side-conditions in "apply in as".
herbelin
2009-10-25
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
- Fixed a bug in checking that implicit arguments are all correctly
herbelin
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
*
Added syntax "exists bindings, ..., bindings" for iterated "exists".
herbelin
2009-09-10
*
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
*
Added "etransitivity".
herbelin
2009-08-03
*
- Fixing bug #2139 (kernel-based test of well-formation of elimination
herbelin
2009-07-15
*
Reactivation of pattern unification of evars in apply unification, in
herbelin
2009-07-08
*
Jolification : tentative de supprimer les "( evd)" et associés qui
aspiwack
2009-07-07
*
Use a lazy value for the message in FailError, so that it won't be
msozeau
2009-06-11
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
Backtrack on experimental unification with sort variables: it requires
msozeau
2009-06-02
*
A try at using sort variables during unification. Instead of refreshing
msozeau
2009-05-23
*
- Fixing declarative mode in presence of high use of Change_evars nodes
herbelin
2009-05-20
*
Minor unification changes:
msozeau
2009-05-18
*
Fixing bug #2308 ("instantiate" tactic did not comply with
herbelin
2009-04-24
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
Cleaning/uniformizing the interface of tacticals.mli
herbelin
2009-03-14
*
commande Timeout + compaction des traces de debug_tactic
barras
2009-03-04
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
pushed evar reduction in kernel
barras
2009-02-06
*
Really compare evar maps in progress, due to merging in apply and other
msozeau
2009-01-23
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- Optimized "auto decomp" which had a (presumably) exponential in
herbelin
2008-12-26
*
Fix looping class resolution bug discovered by B. Aydemir and use the
msozeau
2008-12-14
*
About "apply in":
herbelin
2008-12-09
*
fixing problem with CompCert: reordering resulting from tac change was not cl...
barras
2008-11-27
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
[prev]
[next]