aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenvtac.ml
Commit message (Expand)AuthorAge
...
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* Changement des named_contextGravatar gregoire2005-12-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* simplification de clenvGravatar barras2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03