| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | backtrack unification types et deplacement make_clenv_binding |  filliatr | 2001-03-01 |
| * | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr | 2000-12-12 |
| * | Simplifications autour de typed_type (renommé types par analogie avec sorts)... |  herbelin | 2000-10-18 |
| * | Effets de bords suite à la restructuration des inductives (cf Inductive) | herbelin | 2000-05-18 |
| * | Ajout du langage de tactiques |  delahaye | 2000-05-03 |
| * | - coqmktop | filliatr | 1999-12-03 |
| * | Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations | filliatr | 1999-11-24 |
| * | module Wcclausenv | filliatr | 1999-11-22 |
| * | module Clenv (debut) | filliatr | 1999-10-20 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |