| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-04-21 | Adding a Declare ML Module in empty file Ltac.v. | Hugo Herbelin | |
| Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |