index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
funind
/
tacinv.ml4
Commit message (
Expand
)
Author
Age
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-26
*
More exception handling in functional scheme.
coq
2005-12-08
*
changed the syntax categories of arguments of functional scheme
coq
2005-09-16
*
code cleaning. No changes as far as tested.
coq
2005-08-18
*
Correction of a bug in functional scheme. It raised with mutual
coq
2005-05-26
*
Uniformisation de destApplication en destApp
herbelin
2005-02-12
*
Hugo fixed a bug of refine, and it revealed a bug of functional
coq
2004-12-10
*
Code mort
herbelin
2004-12-06
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1
herbelin
2004-08-24
*
Correction of a bug in Functional Scheme discovered when porting the
coq
2004-02-10
*
New version of Functional Scheme and functional induction. Deals with
coq
2004-02-09
*
Retour des _eq en v8
herbelin
2003-11-27
*
petits changements de syntaxe
barras
2003-11-12
*
Compatibilite V7 des noms d'hypotheses
herbelin
2003-10-07
*
Plus de nom commencant par '_' en V8
herbelin
2003-10-02
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
Correcting a bug occuring when the mimicked function had a
courtieu
2003-03-31
*
Added some tests to make more robust the tactique "Functional
courtieu
2003-03-01
*
The contribution of Pierre Courtieu on generating specialized induction schemes
bertot
2003-02-27