diff options
| author | Maxime Dénès | 2017-12-18 09:38:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 09:38:18 +0100 |
| commit | 3da76841125ef48889c8eceb134116e2d0bd7a2e (patch) | |
| tree | 8728b456dab71560379044459e7a7c979a1b252b /API/API.ml | |
| parent | 0168ee0b6463a9ef44d768b0020b34785986c1cb (diff) | |
| parent | 1172b52735a299dfc91aee36b30b576dfeff581c (diff) | |
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Diffstat (limited to 'API/API.ml')
| -rw-r--r-- | API/API.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/API/API.ml b/API/API.ml index 378c03ee4f..081ac2bb28 100644 --- a/API/API.ml +++ b/API/API.ml @@ -267,7 +267,9 @@ module Metasyntax = Metasyntax module Search = Search (* module Indschemes *) module Obligations = Obligations -module Command = Command +module ComDefinition = ComDefinition +module ComInductive = ComInductive +module ComFixpoint = ComFixpoint module Classes = Classes (* module Record *) (* module Assumptions *) |