index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
decl_proof_instr.ml
Commit message (
Expand
)
Author
Age
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Add more information to IllFormedRecBody exceptions, to show the exact
msozeau
2008-02-08
*
Prise en compte des notations "alias" dans la globalisation des coercions.
herbelin
2007-11-08
*
Ajout de eelim, ecase, edestruct et einduction (expérimental).
herbelin
2007-10-03
*
Declarative language: fixed the generation of fixpoints for induction proofs.
corbinea
2007-07-24
*
extension of the rename tactic: the following is now allowed:
letouzey
2007-07-06
*
Correction d'un bug dans l'affichage du message d'erreur real_clean
herbelin
2007-05-29
*
Contrôle de la compatibilité de apply via une information dans les
herbelin
2007-05-28
*
fixed glitch in escape
corbinea
2007-04-27
*
fin des conclusions multiples
corbinea
2007-04-26
*
debug plus poussé induction dépendante
corbinea
2007-04-18
*
fix bug with dependent inductive families
corbinea
2007-04-16
*
bugfix suffices
corbinea
2007-02-09
*
redirection of errors in coqide + dynamic warning printer (needed for tm_egg)
corbinea
2007-01-31
*
finalized suffices
corbinea
2007-01-29
*
"suffices" implemented + syntax cleanup
corbinea
2007-01-28
*
decl mode: anonymous facts
corbinea
2007-01-25
*
Correction du bug #1315:
notin
2007-01-22
*
changes in declarative language : by term using tactic
corbinea
2007-01-22
*
Raffinement de l'unification de "apply": mémorisation de certains
herbelin
2006-11-19
*
fixed error mesg in decl mode
corbinea
2006-09-26
*
Declarative Proof Language: main commit
corbinea
2006-09-20