index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
plus d'environment fixe cur_env mais un environment evolutif
letouzey
2003-02-02
*
Auto with zarith essaye Abstract Omega sur un but False
filliatr
2003-01-30
*
fignolage
letouzey
2003-01-30
*
pb d'hier resolu. Recommit
letouzey
2003-01-30
*
apres le backtrack precedent, remise de trois points precis et surs
letouzey
2003-01-29
*
Ca a tout pété -> Bactrack a la version d'hier
letouzey
2003-01-29
*
affichage module et module type
letouzey
2003-01-29
*
affichage module et module type
letouzey
2003-01-29
*
affichage module et module type
letouzey
2003-01-29
*
workaround en attendant traitement reel des modules types
letouzey
2003-01-28
*
amelioration du pretty-print des modules
letouzey
2003-01-28
*
nouvelle gestion des constantes de type
letouzey
2003-01-28
*
all tactics should be covered now: remains
bertot
2003-01-26
*
Add translations for many tactics but a dozen are still remaining
bertot
2003-01-25
*
Inspect does not work for pcoq and there is no simple fix because inspect
bertot
2003-01-24
*
The data constructed when detecting an error in a list of commands must
bertot
2003-01-24
*
Corrects the way conjunctions, existential quantifications, and arrows are
bertot
2003-01-24
*
Make sure proof by pointing works.
bertot
2003-01-23
*
Make proof by pointing work for the new notations of existential quantification.
bertot
2003-01-23
*
oubli des add_recursors singleton logiques
letouzey
2003-01-23
*
maj V7.4
letouzey
2003-01-23
*
MAJ
herbelin
2003-01-22
*
removes all references to ctast.ml the Makefile has been updated accordingly.
bertot
2003-01-22
*
petit bug pp haskell
letouzey
2003-01-22
*
Extraction des modules, enfin !
letouzey
2003-01-22
*
Make sure pcoq will also display hypotheses with a value.
bertot
2003-01-21
*
Add a few operators in the new version of xlate.ml and make sure
bertot
2003-01-21
*
Utilisation de 'Recursive' pour les tactiques récursives
herbelin
2003-01-20
*
Simplification de Simplify (plus de ())
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...
herbelin
2003-01-15
*
Export M + Module M <: SIG
coq
2003-01-09
*
SearchAbout
filliatr
2003-01-06
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Petit netoyage dans lib
coq
2002-12-19
*
suppression de l'archive cvs d'un bout de debug
letouzey
2002-12-19
*
les empty ind et les singletons etaient oublies par add_recursors
letouzey
2002-12-19
*
simplification de solve_subgoal: n'utilise plus frontier
barras
2002-12-19
*
stupide inlining des construsteurs
letouzey
2002-12-18
*
Ajout "Locate Notation"
herbelin
2002-12-15
*
Evaluation paresseuse de l'affichage du debug
herbelin
2002-12-15
*
debut de parcours des modules
letouzey
2002-12-13
*
une branche de case inutile
letouzey
2002-12-13
*
Ajout du vernac Proof with
gregoire
2002-12-12
*
Compensation de suppression betaiota de type_of
herbelin
2002-12-11
*
Ajout options -v7 et -v8, et commandes V7only et V8only
herbelin
2002-12-10
*
Normalisation des types (fait avant dans Typing)
herbelin
2002-12-10
*
Ajoute le bon traitement pour Ring, Locate, Comments
bertot
2002-12-09
*
Take notations into account: numbers and the CNotation operator.
bertot
2002-12-09
[next]