index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
romega
/
refl_omega.ml
Age
Commit message (
Expand
)
Author
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2007-07-13
Beginning of a reorganisation of the ml part for romega:
letouzey
2007-07-11
Slight cleanup of refl_omega.ml : in particular it uses now list
letouzey
2007-07-09
Improvements / Bug fixes for ROmega
letouzey
2006-03-24
utilisation de la VM pour la normalisation finale de romega
letouzey
2006-03-23
correctifs de bug pour romega:
letouzey
2006-01-11
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2005-12-26
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-25
Traduction des noms v7 de Z en noms v8
herbelin
2005-11-08
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-02-21
- Correction de bugs
herbelin
2004-12-27
Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)
herbelin
2004-12-27
Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise p...
herbelin
2004-03-04
Reparation ROmega V8/Omega ZERO/POS/NEG
mohring
2004-03-03
adaptation V8 version Pierre Cregut
mohring
2002-12-09
Problèmes et améliorations divers affichage
herbelin
2002-08-02
Modules dans COQ\!\!\!\!
coq
2002-06-03
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-03-01
Prise en compte des corps de letin dans les hypothèses
herbelin
2002-03-01
convert_hyp a change de type
barras
2001-12-13
compat ocaml 3.03
filliatr
2001-09-20
Romega
mohring
2001-09-19
reparation Zne
mohring
2001-09-18
Romega/names/Makefile
mohring