aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenvtac.ml
AgeCommit message (Expand)Author
2006-02-10induction now admits multiple induction arguments. The principle mustcoq
2005-12-02Changement des named_contextgregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-10simplification de clenvbarras
2004-09-08unification encore...barras
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03premiere reorganisation de l\'unificationbarras