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
*
Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)
herbelin
2003-02-01
*
Ajout d'un filtrage d'application partielle
herbelin
2003-01-31
*
MAJ
herbelin
2003-01-31
*
MAJ
herbelin
2003-01-31
*
MAJ
herbelin
2003-01-31
*
Unification plus efficace vis à vis du LetIn
herbelin
2003-01-31
*
preparation pkg deb for 7.4
courant
2003-01-31
*
*** empty log message ***
courant
2003-01-31
*
MAJ syntaxe modules + nouveau fichier mod_decl qui explique tout
coq
2003-01-31
*
Pour satisfaire ProofGeneral
coq
2003-01-31
*
maj
filliatr
2003-01-31
*
Pb de parenthèse dans "Check (S (plus O O))"
herbelin
2003-01-30
*
Adds a possibility to construct a term as if it had been parsed through
bertot
2003-01-30
*
Make sure the parser is compiled in native mode.
bertot
2003-01-30
*
Ajoute les directives pour créer aussi bin/coq-interface.opt
bertot
2003-01-30
*
Auto with zarith essaye Abstract Omega sur un but False
filliatr
2003-01-30
*
changement de place du Initial State (maintenant apres l'analyse de la ligne ...
filliatr
2003-01-30
*
pas de Xml.vo
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
*
MAJ pour Reg
desmettr
2003-01-28
*
Deux p\'tits trucs ;)
coq
2003-01-27
*
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
*
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
[next]