index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2000-05-18
Restructuration des outils pour les inductifs.
herbelin
2000-05-18
Ajout lift_context
herbelin
2000-05-18
Effets de bords suite à la restructuration des inductives (cf Inductive)
herbelin
2000-05-18
Centralisation prod_name and co dans Environ; mkLambda_string dans Term
herbelin
2000-05-18
Adaptation pour nouveaux inductifs (cf Inductive)
herbelin
2000-05-18
Nettoyage
herbelin
2000-05-18
Restructuration des outils pour les inductifs.
herbelin
2000-05-18
Centralisation prod_name and co dans Environ; mkLambda_string dans Term
herbelin
2000-05-18
doc
herbelin
2000-05-16
Ajout mis_typepath
herbelin
2000-05-16
Retrait du i pour tclTHEN_i et correction bugs Decompose
herbelin
2000-05-16
RIEN
herbelin
2000-05-16
Rien
herbelin
2000-05-08
contrib linkees en natif
filliatr
2000-05-08
un Declare ML Module inutile
filliatr
2000-05-05
ajout d'Inversion
filliatr
2000-05-05
MAJ
herbelin
2000-05-05
doc
herbelin
2000-05-05
Ajout d'un strong 'light'
herbelin
2000-05-05
ajout interp_sort
herbelin
2000-05-05
Réorganisation
herbelin
2000-05-05
Achèvement nettoyage Pfedit; ajout intros_replacing
herbelin
2000-05-05
Intégration de leminv
herbelin
2000-05-05
Achèvement nettoyage Pfedit
herbelin
2000-05-05
Ajoute option -byte
herbelin
2000-05-04
MAJ
herbelin
2000-05-04
Vernacinterp passe après Command
herbelin
2000-05-04
les erreurs
herbelin
2000-05-04
Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)
herbelin
2000-05-04
Nettoyage de l'interface de Pfedit
herbelin
2000-05-03
nettoyage (quelques oublis dans make clean)
filliatr
2000-05-03
compilation bytecode / native :
filliatr
2000-05-03
Retrait de PrintConstr vers top_printers
delahaye
2000-05-03
Completion d'un match non exhaustif
delahaye
2000-05-03
Ajout de PrintConstr pour debug
delahaye
2000-05-03
Reparation du bug d'interpretation d'Abstract
delahaye
2000-05-03
diverses modifs pour ocamlweb
filliatr
2000-05-03
MAJ
herbelin
2000-05-03
retour a la version qui ne contournait pas le bug de PatternMatchingFailure n...
herbelin
2000-05-03
suppression de Fw pour les implicites
herbelin
2000-05-03
Ajout get_reference
herbelin
2000-05-03
Encapsulage de PatternMatchingFailure par un 'error' pour que l'echec de conc...
herbelin
2000-05-03
renommage de certains printers
herbelin
2000-05-03
Ajout du langage de tactiques
delahaye
2000-05-02
portage Omega (mais toujours pas Zpower et Zlogarithm)
filliatr
2000-05-02
construct_reference prend en compte aussi les variables du context
filliatr
2000-05-02
pattern-matching non-exhaustif (occur_rawconstr)
filliatr
2000-05-02
Divers
herbelin
2000-05-02
Problème avec SOPATT
herbelin
2000-05-02
Problème avec motif du second-ordre
herbelin
[next]