diff options
| author | Emilio Jesus Gallego Arias | 2017-07-31 14:24:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-08-29 17:39:41 +0200 |
| commit | 028de158153de94adfcb9d1e995259d833968951 (patch) | |
| tree | 0f02a6c03094971a3c095795e6a190618e470d45 /API/API.mli | |
| parent | cc58638a8d33084c5c9f85ab4d536307da2d7929 (diff) | |
[general] Merge parsing with highparsing, put toplevel at the top of the linking chain.
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 44 |
1 files changed, 18 insertions, 26 deletions
diff --git a/API/API.mli b/API/API.mli index 3b2dc5a679..a80de7b2c9 100644 --- a/API/API.mli +++ b/API/API.mli @@ -10,7 +10,7 @@ in Coq. To see such order issue the comand: ``` - bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done && echo -e "\n## highparsing files" && cat parsing/highparsing.mllib' > API/link + bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link ``` Note however that files in intf/ are located manually now as their @@ -4828,6 +4828,23 @@ sig end +module G_vernac : +sig + + val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry + val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry + val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry + +end + +module G_proofs : +sig + + val hint : Vernacexpr.hints_expr Pcoq.Gram.entry + val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option + +end + (************************************************************************) (* End of modules from parsing/ *) (************************************************************************) @@ -5717,28 +5734,3 @@ end (************************************************************************) (* End of modules from stm/ *) (************************************************************************) - -(************************************************************************) -(* Modules from highparsing/ *) -(************************************************************************) - -module G_vernac : -sig - - val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry - val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry - val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry - -end - -module G_proofs : -sig - - val hint : Vernacexpr.hints_expr Pcoq.Gram.entry - val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option - -end - -(************************************************************************) -(* End of modules from highparsing/ *) -(************************************************************************) |