| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-05 | Merge numeral and string notation plugins | Pierre Roux | |
| 2018-08-31 | Move g_numeral.ml4 to numeral.ml | Jason Gross | |
| As per https://github.com/coq/coq/pull/8064#pullrequestreview-145971522 | |||
| 2018-08-31 | Numeral Notation (for inductive types) | Pierre Letouzey | |
| This is a portion of roglo's PR#156 introducing a Numeral Notation command : we deal here with inductive types via conversion fonctions from/to Z written in Coq. For an example, see plugins/syntax/NatSyntaxViaZ.v This commit does not include the part about printing via some ltac. Using ltac was meant for dealing with real numbers, let's see first what become PR#415 about a compact representation for real literals. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |