diff options
| author | vsiles | 2007-05-25 14:47:02 +0000 |
|---|---|---|
| committer | vsiles | 2007-05-25 14:47:02 +0000 |
| commit | 46dcebf37f85781cc7f622f1bec7314bc6af26d5 (patch) | |
| tree | b2d2fb246e0a2b3dbf932ca7409ccbc0646a8890 /doc/RecTutorial | |
| parent | db50dfc5e752f7209c10256d8af86f24677221d1 (diff) | |
Modification of VernacScheme to handle a new scheme: Equality (equality in
boolean, will be added later) and update so everything is fine with the new
syntax.
New Type:
type scheme =
| InductionScheme of bool * lreference * sort_expr
| EqualityScheme of lreference
...
| VernacScheme of (lident * scheme) list
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RecTutorial')
0 files changed, 0 insertions, 0 deletions