index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Add translations for many tactics but a dozen are still remaining
bertot
2003-01-25
*
Un type "standardisé" pour new_hyp
herbelin
2003-01-25
*
Inspect does not work for pcoq and there is no simple fix because inspect
bertot
2003-01-24
*
on cree toujours le sous-repertoire tactics/
filliatr
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
*
maj
filliatr
2003-01-24
*
Make sure proof by pointing works.
bertot
2003-01-23
*
reparation des contribs: lors de l'unification, reduire les beta redexes
barras
2003-01-23
*
Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).
corbinea
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
*
status de l'extraction
letouzey
2003-01-23
*
maj V7.4
letouzey
2003-01-23
*
MAJ
herbelin
2003-01-22
*
Mauvais environnement d'évaluation pour les globaux
herbelin
2003-01-22
*
*** empty log message ***
barras
2003-01-22
*
modified the unification algorithm to try first order unification before
barras
2003-01-22
*
Documentation du contenu de REALS
desmettr
2003-01-22
*
ajout de whd_state dans l'interface
barras
2003-01-22
*
Changements dans REALS
desmettr
2003-01-22
*
removes all references to ctast.ml the Makefile has been updated accordingly.
bertot
2003-01-22
*
Modifications dans SeqProp
desmettr
2003-01-22
*
Renommages dans Rtrigo_def
desmettr
2003-01-22
*
I changed the interface to make sure SearchAbout is defined according to
bertot
2003-01-22
*
Commentaires
desmettr
2003-01-22
*
Renommages nombreux
desmettr
2003-01-22
*
Commentaires
desmettr
2003-01-22
*
Correction bug réecriture à la racine pour le sétoide Prop.
clrenard
2003-01-22
*
Renommage f_pos -> IVT (Intermediate Value Theorem
desmettr
2003-01-22
*
Suppression d'un Import R_scope probablement oublie
desmettr
2003-01-22
*
Commentaires
desmettr
2003-01-22
*
Renommages dans RList
desmettr
2003-01-22
*
MAJ pour renommage Rcomplet
desmettr
2003-01-22
*
Renommages dans Rcomplete
desmettr
2003-01-22
*
Renommage Rcomplet.v -> Rcomplete.v
desmettr
2003-01-22
*
Suppression de lemmes superflus
desmettr
2003-01-22
*
Commentaires
desmettr
2003-01-22
*
Renommages dans PartSum
desmettr
2003-01-22
*
Bug 'with Module' corrige
coq
2003-01-22
*
Bug precedence
herbelin
2003-01-22
*
petit bug pp haskell
letouzey
2003-01-22
*
maj
filliatr
2003-01-22
*
Extraction des modules, enfin !
letouzey
2003-01-22
*
id_of_msid en plus
letouzey
2003-01-22
*
Adaptation à la nouvelle sémantique plus uniforme de "Match term"
herbelin
2003-01-21
*
Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur
herbelin
2003-01-21
*
portabilite
doligez
2003-01-21
*
Renommage dans MVT
desmettr
2003-01-21
*
MAJ dans Exp_prop
desmettr
2003-01-21
[next]