aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-16 13:54:13 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-16 13:54:13 +0200
commit978dd21af8467aa483bce551b3d5df8895cfff0f (patch)
tree41f473bddf855d3daf179c83ed63166834ae3240 /ide
parent89f7bc53fbd558e3b5ff2ce1d1693f570afcc536 (diff)
parent7bd00a63015c4017d8209a4d495b9683d33d1d53 (diff)
Make the Coq codebase independent from Ltac-related code.
We untangle many dependencies on Ltac datastructures and modules from the lower strata, resulting in a self-contained ltac/ folder. While not a plugin yet, the change is now very easy to perform. The main API changes have been documented in the dev/doc/changes file. The patches are quite rough, and it may be the case that some parts of the code can migrate back from ltac/ to a core folder. This should be decided on a case-by-case basis, according to a more long-term consideration of what is exactly Ltac-dependent and whatnot.
Diffstat (limited to 'ide')
-rw-r--r--ide/richprinter.ml1
-rw-r--r--ide/texmacspp.ml6
2 files changed, 1 insertions, 6 deletions
diff --git a/ide/richprinter.ml b/ide/richprinter.ml
index 5f39f36ea..995cef1ac 100644
--- a/ide/richprinter.ml
+++ b/ide/richprinter.ml
@@ -2,7 +2,6 @@ open Richpp
module RichppConstr = Ppconstr.Richpp
module RichppVernac = Ppvernac.Richpp
-module RichppTactic = Pptactic.Richpp
type rich_pp =
Ppannotation.t Richpp.located Xml_datatype.gxml
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 53a29008a..328ddd0cd 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -127,10 +127,6 @@ let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
-let xmlRawTactic name rtac =
- Element("rawtactic", ["name",name],
- [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
-
let xmlSectionSubsetDescr name ssd =
Element("sectionsubsetdescr",["name",name],
[PCData (Proof_using.to_string ssd)])
@@ -742,7 +738,7 @@ let rec tmpp v loc =
| VernacShow _ as x -> xmlTODO loc x
| VernacCheckGuard as x -> xmlTODO loc x
| VernacProof (tac,using) ->
- let tac = Option.map (xmlRawTactic "closingtactic") tac in
+ let tac = None (** FIXME *) in
let using = Option.map (xmlSectionSubsetDescr "using") using in
xmlProof loc (Option.List.(cons tac (cons using [])))
| VernacProofMode name -> xmlProofMode loc name