index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_proofs.ml4
Commit message (
Expand
)
Author
Age
*
compat ocaml 3.03
filliatr
2001-12-13
*
Retablissement de la commande Existential que j'avais supprime par erreur.
clrenard
2001-11-23
*
Diverses petites simplications de la machine de preuves.
clrenard
2001-11-19
*
Prise en compte qualid dans Hint Unfold
herbelin
2001-09-13
*
ajout Show Intro(s)
letouzey
2001-07-04
*
Fix de quelques bugs syntaxiques de Ltac
delahaye
2001-06-11
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
entetes
filliatr
2001-03-15
*
Factorisation du '.' final
herbelin
2001-01-27
*
Prise en compte des noms longs dans les Hints et les Coercions
herbelin
2001-01-24
*
Meta Definition + Tactic Definition
delahaye
2001-01-09
*
Arite cachee de Match Context + Meta Definition
delahaye
2001-01-05
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
Nouveau mode de compilation de .ml4
herbelin
2000-11-05
*
Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...
herbelin
2000-11-05