Merge PR#708: [ide] Correct merging error.

2 files changed, 0 insertions, 781 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
deleted file mode 100644
index ddb62313f..000000000
--- a/ide/texmacspp.ml
+++ /dev/null
@@ -1,769 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-open Constrexpr
-open Names
-open Misctypes
-open Bigint
-open Decl_kinds
-open Extend
-open Libnames
-open Constrexpr_ops
-
-let unlock ?loc =
-  let start, stop = Option.cata Loc.unloc (0,0) loc in
-  (string_of_int start, string_of_int stop)
-
-let xmlWithLoc ?loc ename attr xml =
-  let start, stop = unlock ?loc in
-  Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
-
-let get_fst_attr_in_xml_list attr xml_list =
-  let attrs_list =
-    List.map (function
-      | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
-      | _ -> [])
-    xml_list in
-  match List.flatten attrs_list with
-  | [] -> (attr, "")
-  | l  -> (List.hd l)
-
-let backstep_loc xmllist =
-  let start_att = get_fst_attr_in_xml_list "begin" xmllist in
-  let stop_att =  get_fst_attr_in_xml_list "end" (List.rev xmllist) in
-  [start_att ; stop_att]
-
-let compare_begin_att xml1 xml2 =
-  let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
-  let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
-  match att1, att2 with
-  | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
-  | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
-  | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
-  | _ -> 0
-
-let xmlBeginSection ?loc name = xmlWithLoc ?loc "beginsection" ["name", name] []
-
-let xmlEndSegment ?loc name = xmlWithLoc ?loc "endsegment" ["name", name] []
-
-let xmlThm ?loc typ name xml =
-  xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml
-
-let xmlDef ?loc typ name xml =
-  xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml
-
-let xmlNotation ?loc attr name xml =
-  xmlWithLoc ?loc "notation" (("name", name) :: attr) xml
-
-let xmlReservedNotation ?loc attr name =
-  xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) []
-
-let xmlCst ?loc ?(attr=[]) name =
-  xmlWithLoc ?loc "constant" (("name", name) :: attr) []
-
-let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name =
-  xmlWithLoc ?loc "operator"
-    (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
-
-let xmlApply ?loc ?(attr=[]) xml = xmlWithLoc ?loc "apply" attr xml
-
-let xmlToken ?loc ?(attr=[]) xml = xmlWithLoc ?loc "token" attr xml
-
-let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
-
-let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
-
-let xmlCase xml = Element("case", [], xml)
-
-let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
-
-let xmlWith xml = Element("with", [], xml)
-
-let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
-
-let xmlInductive ?loc kind xml = xmlWithLoc ?loc "inductive" ["kind",kind] xml
-
-let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
-
-let xmlFixpoint xml = Element("fixpoint", [], xml)
-
-let xmlCheck ?loc xml = xmlWithLoc ?loc "check" [] xml
-
-let xmlAssumption ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml
-
-let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml
-
-let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr []
-
-let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr []
-
-let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] []
-
-let xmlReference ref =
-  let name = Libnames.string_of_reference ref in
-  let i, j = Option.cata Loc.unloc (0,0) (Libnames.loc_of_reference ref) in
-  let b, e = string_of_int i, string_of_int j in
-  Element("reference",["name", name; "begin", b; "end", e] ,[])
-
-let xmlRequire ?loc ?(attr=[]) xml = xmlWithLoc ?loc "require" attr xml
-let xmlImport ?loc ?(attr=[]) xml = xmlWithLoc ?loc "import" attr xml
-
-let xmlAddLoadPath ?loc ?(attr=[]) xml = xmlWithLoc ?loc "addloadpath" attr xml
-let xmlRemoveLoadPath ?loc ?(attr=[]) = xmlWithLoc ?loc "removeloadpath" attr
-let xmlAddMLPath ?loc ?(attr=[]) = xmlWithLoc ?loc "addmlpath" attr
-
-let xmlExtend ?loc xml = xmlWithLoc ?loc "extend" [] xml
-
-let xmlScope ?loc ?(attr=[]) action name xml =
-  xmlWithLoc ?loc "scope" (["name",name;"action",action] @ attr) xml
-
-let xmlProofMode ?loc name = xmlWithLoc ?loc "proofmode" ["name",name] []
-
-let xmlProof ?loc xml = xmlWithLoc ?loc "proof" [] xml
-
-let xmlSectionSubsetDescr name ssd =
-  Element("sectionsubsetdescr",["name",name],
-    [PCData (Proof_using.to_string ssd)])
-
-let xmlDeclareMLModule ?loc s =
-  xmlWithLoc ?loc "declarexmlmodule" []
-    (List.map (fun x -> Element("path",["value",x],[])) s)
-
-(* tactics *)
-let xmlLtac ?loc xml = xmlWithLoc ?loc "ltac" [] xml
-
-(* toplevel commands *)
-let xmlGallina ?loc xml = xmlWithLoc ?loc "gallina" [] xml
-
-let xmlTODO ?loc x =
-  xmlWithLoc ?loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-let string_of_name n =
-  match n with
-  | Anonymous -> "_"
-  | Name id -> Id.to_string id
-
-let string_of_glob_sort s =
-  match s with
-  | GProp -> "Prop"
-  | GSet -> "Set"
-  | GType _ -> "Type"
-
-let string_of_cast_sort c =
-  match c with
-  | CastConv _ -> "CastConv"
-  | CastVM _ -> "CastVM"
-  | CastNative _ -> "CastNative"
-  | CastCoerce -> "CastCoerce"
-
-let string_of_case_style s =
-  match s with
-  | LetStyle -> "Let"
-  | IfStyle -> "If"
-  | LetPatternStyle -> "LetPattern"
-  | MatchStyle -> "Match"
-  | RegularStyle -> "Regular"
-
-let attribute_of_syntax_modifier sm =
-match sm with
-  | SetItemLevel (sl, NumLevel n) ->
-      List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
-  | SetItemLevel (sl, NextLevel) ->
-      List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
-  | SetLevel i -> ["level", string_of_int i]
-  | SetAssoc a ->
-      begin match a with
-      | NonA -> ["",""]
-      | RightA -> ["associativity", "right"]
-      | LeftA -> ["associativity", "left"]
-      end
-  | SetEntryType (s, _) -> ["entrytype", s]
-  | SetOnlyPrinting -> ["onlyprinting", ""]
-  | SetOnlyParsing -> ["onlyparsing", ""]
-  | SetCompatVersion v -> ["compat", Flags.pr_version v]
-  | SetFormat (system, (loc, s)) ->
-      let start, stop = unlock ?loc in
-      ["format-"^system, s; "begin", start; "end", stop]
-
-let string_of_assumption_kind l a many =
-  match l, a, many with
-  | (Discharge, Logical,      true)  -> "Hypotheses"
-  | (Discharge, Logical,      false) -> "Hypothesis"
-  | (Discharge, Definitional, true)  -> "Variables"
-  | (Discharge, Definitional, false) -> "Variable"
-  | (Global,    Logical,      true)  -> "Axioms"
-  | (Global,    Logical,      false) -> "Axiom"
-  | (Global,    Definitional, true)  -> "Parameters"
-  | (Global,    Definitional, false) -> "Parameter"
-  | (Local,     Logical,      true)  -> "Local Axioms"
-  | (Local,     Logical,      false) -> "Local Axiom"
-  | (Local,     Definitional, true)  -> "Local Parameters"
-  | (Local,     Definitional, false) -> "Local Parameter"
-  | (Global,    Conjectural, _)      -> "Conjecture"
-  | ((Discharge | Local), Conjectural, _) -> assert false
-
-let rec pp_bindlist bl =
-  let tlist =
-    List.flatten
-        (List.map
-          (fun (loc_names, _, e) ->
-            let names =
-              (List.map
-                (fun (loc, name) ->
-                  xmlCst ?loc (string_of_name name)) loc_names) in
-            match e.CAst.v with
-              | CHole _ -> names
-              | _ -> names @ [pp_expr e])
-          bl) in
-  match tlist with
-    | [e] -> e
-    | l -> xmlTyped l
-and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
-  Element ("decl_notation", ["name", s], [pp_expr ce])
-and pp_local_binder lb = (* don't know what it is for now *)
-  match lb with
-  | CLocalDef ((loc, nam), ce, ty) ->
-      let attrs = ["name", string_of_name nam] in
-      let value = match ty with
-          Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t)
-        | None -> ce in
-      pp_expr ~attr:attrs value
-  | CLocalAssum (namll, _, ce) ->
-      let ppl =
-        List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in
-      xmlTyped (ppl @ [pp_expr ce])
-  | CLocalPattern _ ->
-      assert false
-and pp_local_decl_expr lde = (* don't know what it is for now *)
-  match lde with
-  | AssumExpr (_, ce)  -> pp_expr ce
-  | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
-  (* inductive_expr *)
-  let b,e = Option.cata Loc.unloc (0,0) l in
-  let location = ["begin", string_of_int b; "end", string_of_int e] in
-  [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
-  begin match cl_or_rdexpr with
-  | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
-  | RecordDecl (_, ldewwwl) ->
-      List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
-  end @
-  begin match ceo with (* don't know what it is for now *)
-  | Some ce -> [pp_expr ce]
-  | None -> []
-  end @
-  (List.map pp_local_binder lbl)
-and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
-  let attrs =
-    match optid with
-    | None -> []
-    | Some (loc, id) ->
-        let start, stop = unlock ?loc in
-        ["begin", start; "end", stop ; "name", Id.to_string id] in
-  let kind, expr =
-    match roe with
-    | CStructRec -> "struct", []
-    | CWfRec e -> "rec", [pp_expr e]
-    | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
-    | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
-  Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
-  (* fixpoint_expr *)
-  let start, stop = unlock ?loc in
-  let id = Id.to_string id in
-  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
-  (* fixpoint name *)
-  [pp_recursion_order_expr optid roe] @
-  (List.map pp_local_binder lbl) @
-  [pp_expr ce] @
-  begin match ceo with (* don't know what it is for now *)
-  | Some ce -> [pp_expr ce]
-  | None -> []
-  end
-and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
-  (* Nota: it is like fixpoint_expr without (optid, roe)
-   * so could be merged if there is no more differences *)
-  let start, stop = unlock ?loc in
-  let id = Id.to_string id in
-  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
-  (* cofixpoint name *)
-  (List.map pp_local_binder lbl) @
-  [pp_expr ce] @
-  begin match ceo with (* don't know what it is for now *)
-  | Some ce -> [pp_expr ce]
-  | None -> []
-  end
-and pp_lident (loc, id) = xmlCst ?loc (Id.to_string id)
-and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr {loc ; CAst.v = cpe} =
-  match cpe with
-  | CPatAlias (cpe, id) ->
-      xmlApply ?loc
-        (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" ::
-          [pp_cases_pattern_expr cpe])
-  | CPatCstr (ref, None, cpel2) ->
-      xmlApply ?loc
-        (xmlOperator ?loc "reference"
-           ~attr:["name", Libnames.string_of_reference ref] ::
-         [Element ("impargs", [], []);
-          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
-  | CPatCstr (ref, Some cpel1, cpel2) ->
-      xmlApply ?loc
-        (xmlOperator ?loc "reference"
-           ~attr:["name", Libnames.string_of_reference ref] ::
-         [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
-          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
-  | CPatAtom optr ->
-      let attrs = match optr with
-        | None -> []
-        | Some r -> ["name", Libnames.string_of_reference r] in
-      xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: [])
-  | CPatOr cpel ->
-      xmlApply ?loc (xmlOperator ?loc "or" :: List.map pp_cases_pattern_expr cpel)
-  | CPatNotation (n, (subst_constr, subst_rec), cpel) ->
-      xmlApply ?loc
-        (xmlOperator ?loc "notation" ::
-          [xmlOperator ?loc n;
-           Element ("subst", [],
-             [Element ("subterms", [],
-                List.map pp_cases_pattern_expr subst_constr);
-              Element ("recsubterms", [],
-                List.map
-                  (fun (cpel) ->
-                     Element ("recsubterm", [],
-                       List.map pp_cases_pattern_expr cpel))
-                subst_rec)]);
-           Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
-  | CPatPrim tok   -> pp_token ?loc tok
-  | CPatRecord rcl ->
-      xmlApply ?loc
-        (xmlOperator ?loc "record" ::
-           List.map (fun (r, cpe) ->
-             Element ("field",
-               ["reference", Libnames.string_of_reference r],
-               [pp_cases_pattern_expr cpe]))
-           rcl)
-  | CPatDelimiters (delim, cpe) ->
-      xmlApply ?loc
-        (xmlOperator ?loc "delimiter" ~attr:["name", delim] ::
-          [pp_cases_pattern_expr cpe])
-  | CPatCast _ -> assert false
-and pp_case_expr (e, name, pat) =
-  match name, pat with
-  | None, None -> xmlScrutinee [pp_expr e]
-  | Some (loc, name), None ->
-      let start, stop= unlock ?loc in
-      xmlScrutinee ~attr:["name", string_of_name name;
-                          "begin", start; "end", stop] [pp_expr e]
-  | Some (loc, name), Some p ->
-      let start, stop= unlock ?loc in
-      xmlScrutinee ~attr:["name", string_of_name name;
-                          "begin", start; "end", stop]
-        [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-  | None, Some p ->
-      xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-and pp_branch_expr_list bel =
-  xmlWith
-    (List.map
-      (fun (_, (cpel, e)) ->
-        let ppcepl =
-          List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
-        let ppe = [pp_expr e] in
-        xmlCase (ppcepl @ ppe))
-     bel)
-and pp_token ?loc tok =
-  let tokstr =
-    match tok with
-    | String s -> PCData s
-    | Numeral n -> PCData (to_string n) in
-  xmlToken ?loc [tokstr]
-and pp_local_binder_list lbl =
-  let l = (List.map pp_local_binder lbl) in
-  Element ("recurse", (backstep_loc l), l)
-and pp_const_expr_list cel =
-  let l = List.map pp_expr cel in
-  Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) { loc; CAst.v = e } =
-  match e with
-  | CRef (r, _) ->
-      xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r)
-  | CProdN (bl, e) ->
-      xmlApply ?loc
-        (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e])
-  | CApp ((_, hd), args) ->
-       xmlApply ?loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
-  | CAppExpl ((_, r, _), args) ->
-       xmlApply ?loc ~attr
-         (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r)
-                 :: List.map pp_expr args)
-  | CNotation (notation,  ([],[],[])) ->
-       xmlOperator ?loc notation
-  | CNotation (notation,  (args, cell, lbll)) ->
-      let fmts = Notation.find_notation_extra_printing_rules notation in
-      let oper = xmlOperator ?loc notation ~pprules:fmts in
-      let cels = List.map pp_const_expr_list cell in
-      let lbls = List.map pp_local_binder_list lbll in
-      let args = List.map pp_expr args in
-      xmlApply ?loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
-  | CSort(s) ->
-      xmlOperator ?loc (string_of_glob_sort s)
-  | CDelimiters (scope, ce) ->
-      xmlApply ?loc (xmlOperator ?loc "delimiter" ~attr:["name", scope] ::
-        [pp_expr ce])
-  | CPrim tok -> pp_token ?loc tok
-  | CGeneralization (kind, _, e) ->
-      let kind= match kind with
-      | Explicit -> "explicit"
-      | Implicit -> "implicit" in
-      xmlApply ?loc
-        (xmlOperator ?loc ~attr:["kind", kind] "generalization" :: [pp_expr e])
-  | CCast (e, tc) ->
-      begin match tc with
-      | CastConv t | CastVM t |CastNative t ->
-          xmlApply ?loc
-            (xmlOperator ?loc ":" ~attr:["kind", (string_of_cast_sort tc)] ::
-             [pp_expr e; pp_expr t])
-      | CastCoerce   ->
-          xmlApply ?loc
-            (xmlOperator ?loc ":" ~attr:["kind", "CastCoerce"] ::
-             [pp_expr e])
-      end
-  | CEvar (ek, cel) ->
-      let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
-      xmlApply ?loc
-        (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] ::
-          ppcel)
-  | CPatVar id -> xmlPatvar ?loc (string_of_id id)
-  | CHole (_, _, _) -> xmlCst ?loc ~attr  "_"
-  | CIf (test, (_, ret), th, el) ->
-      let return = match ret with
-      | None -> []
-      | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply ?loc
-        (xmlOperator ?loc "if" ::
-          return @ [pp_expr th] @ [pp_expr el])
-  | CLetTuple (names, (_, ret), value, body) ->
-      let return = match ret with
-      | None -> []
-      | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply ?loc
-        (xmlOperator ?loc "lettuple" ::
-          return @
-          (List.map (fun (loc, var) -> xmlCst ?loc (string_of_name var)) names) @
-          [pp_expr value; pp_expr body])
-  | CCases (sty, ret, cel, bel) ->
-      let return = match ret with
-      | None -> []
-      | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply ?loc
-        (xmlOperator ?loc ~attr:["style", (string_of_case_style sty)] "match" ::
-          (return @
-           [Element ("scrutinees", [], List.map pp_case_expr cel)] @
-           [pp_branch_expr_list bel]))
-  | CRecord _ -> assert false
-  | CLetIn ((varloc, var), value, typ, body) ->
-      let value = match typ with
-        | Some t ->
-          CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t))
-        | None -> value in
-      xmlApply ?loc
-        (xmlOperator ?loc "let" ::
-         [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body])
-  | CLambdaN (bl, e) ->
-      xmlApply ?loc
-        (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e])
-  | CCoFix (_, _) -> assert false
-  | CFix (lid, fel) ->
-      xmlApply ?loc
-        (xmlOperator ?loc "fix" ::
-           List.flatten (List.map
-             (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
-             fel))
-
-let pp_comment c =
-  match c with
-  | CommentConstr e -> [pp_expr e]
-  | CommentString s -> [Element ("string", [], [PCData s])]
-  | CommentInt i    -> [PCData (string_of_int i)]
-
-let rec tmpp ?loc v =
-  match v with
-  (* Control *)
-  | VernacLoad (verbose,f) ->
-      xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] []
-  | VernacTime (loc,e) ->
-      xmlApply ?loc (Element("time",[],[]) ::
-                    [tmpp ?loc e])
-  | VernacRedirect (s, (loc,e)) ->
-      xmlApply ?loc (Element("redirect",["path", s],[]) ::
-                    [tmpp ?loc e])
-  | VernacTimeout (s,e) ->
-      xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) ::
-                    [tmpp ?loc e])
-  | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e])
-
-  (* Syntax *)
-  | VernacSyntaxExtension (_, ((_, name), sml)) ->
-      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
-      xmlReservedNotation ?loc attrs name
-
-  | VernacOpenCloseScope (_,(true,name)) -> xmlScope ?loc "open" name []
-  | VernacOpenCloseScope (_,(false,name)) -> xmlScope ?loc "close" name []
-  | VernacDelimiters (name,Some tag) ->
-      xmlScope ?loc "delimit" name ~attr:["delimiter",tag] []
-  | VernacDelimiters (name,None) ->
-      xmlScope ?loc "undelimit" name ~attr:[] []
-  | VernacInfix (_,((_,name),sml),ce,sn) ->
-      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
-      let sc_attr =
-        match sn with
-        | Some scope -> ["scope", scope]
-        | None -> [] in
-      xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce]
-  | VernacNotation (_, ce, (lstr, sml), sn) ->
-      let name = snd lstr in
-      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
-      let sc_attr =
-        match sn with
-        | Some scope -> ["scope", scope]
-        | None -> [] in
-      xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce]
-  | VernacBindScope _ as x -> xmlTODO ?loc x
-  | VernacNotationAddFormat _ as x -> xmlTODO ?loc x
-  | VernacUniverse _
-  | VernacConstraint _
-  | VernacPolymorphic (_, _) as x -> xmlTODO ?loc x
-  (* Gallina *)
-  | VernacDefinition (ldk, ((_,id),_), de) ->
-      let l, dk =
-        match ldk with
-        | Some l, dk -> (l, dk)
-        | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
-      let e =
-        match de with
-        | ProveBody (_, ce) -> ce
-        | DefineBody (_, Some _, ce, None) -> ce
-        | DefineBody (_, None  , ce, None) -> ce
-        | DefineBody (_, Some _, ce, Some _) -> ce
-        | DefineBody (_, None  , ce, Some _) -> ce in
-      let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
-      let str_id = Id.to_string id in
-      (xmlDef ?loc str_dk str_id [pp_expr e])
-  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
-      let str_tk = Kindops.string_of_theorem_kind tk in
-      let str_id = Id.to_string id in
-      (xmlThm ?loc str_tk str_id [pp_expr statement])
-  | VernacStartTheoremProof _ as x -> xmlTODO ?loc x
-  | VernacEndProof pe ->
-      begin
-        match pe with
-        | Admitted -> xmlQed ?loc ?attr:None
-        | Proved (_, Some ((_, id), Some tk)) ->
-            let nam = Id.to_string id in
-            let typ = Kindops.string_of_theorem_kind tk in
-            xmlQed ?loc ~attr:["name", nam; "type", typ]
-        | Proved (_, Some ((_, id), None)) ->
-            let nam = Id.to_string id in
-            xmlQed ?loc ~attr:["name", nam]
-        | Proved _ -> xmlQed ?loc ?attr:None
-      end
-  | VernacExactProof _ as x -> xmlTODO ?loc x
-  | VernacAssumption ((l, a), _, sbwcl) ->
-      let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
-      let many =
-        List.length (List.flatten (List.map fst binders)) > 1 in
-      let exprs =
-        List.flatten (List.map pp_simple_binder binders) in
-      let l = match l with Some x -> x | None -> Decl_kinds.Global in
-      let kind = string_of_assumption_kind l a many in
-      xmlAssumption ?loc kind exprs
-  | VernacInductive (_, _, iednll) ->
-      let kind =
-        let (_, _, _, k, _), _ = List.hd iednll in
-	  begin
-            match k with
-            | Record -> "Record"
-            | Structure -> "Structure"
-            | Inductive_kw -> "Inductive"
-            | CoInductive -> "CoInductive"
-            | Class _ -> "Class"
-            | Variant -> "Variant"
-          end in
-      let exprs =
-        List.flatten (* should probably not be flattened *)
-          (List.map
-            (fun (ie, dnl) -> (pp_inductive_expr ie) @
-                              (List.map pp_decl_notation dnl)) iednll) in
-      xmlInductive ?loc kind exprs
-  | VernacFixpoint (_, fednll) ->
-      let exprs =
-        List.flatten (* should probably not be flattened *)
-          (List.map
-            (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
-                              (List.map pp_decl_notation dnl)) fednll) in
-      xmlFixpoint exprs
-  | VernacCoFixpoint (_, cfednll) ->
-      (* Nota: it is like VernacFixpoint without so could be merged *)
-      let exprs =
-        List.flatten (* should probably not be flattened *)
-          (List.map
-            (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
-                              (List.map pp_decl_notation dnl)) cfednll) in
-      xmlCoFixpoint exprs
-  | VernacScheme _ as x -> xmlTODO ?loc x
-  | VernacCombinedScheme _ as x -> xmlTODO ?loc x
-
-  (* Gallina extensions *)
-  | VernacBeginSection (_, id) -> xmlBeginSection ?loc (Id.to_string id)
-  | VernacEndSegment (_, id) -> xmlEndSegment ?loc (Id.to_string id)
-  | VernacNameSectionHypSet _ as x -> xmlTODO ?loc x
-  | VernacRequire (from, import, l) ->
-      let import = match import with
-      | None -> []
-      | Some true -> ["export","true"]
-      | Some false -> ["import","true"]
-      in
-      let from = match from with
-      | None -> []
-      | Some r -> ["from", Libnames.string_of_reference r]
-      in
-      xmlRequire ?loc ~attr:(from @ import) (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacImport (true,l) ->
-      xmlImport ?loc ~attr:["export","true"] (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacImport (false,l) ->
-      xmlImport ?loc (List.map (fun ref -> xmlReference ref) l)
-  | VernacCanonical r ->
-      let attr =
-        match r with
-        | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
-        | AN (Ident (_, id)) -> ["id", Id.to_string id]
-        | ByNotation (_, (s, _)) -> ["notation", s] in
-      xmlCanonicalStructure ?loc attr
-  | VernacCoercion _ as x -> xmlTODO ?loc x
-  | VernacIdentityCoercion _ as x -> xmlTODO ?loc x
-
-  (* Type classes *)
-  | VernacInstance _ as x -> xmlTODO ?loc x
-
-  | VernacContext _ as x -> xmlTODO ?loc x
-
-  | VernacDeclareInstances _ as x -> xmlTODO ?loc x
-
-  | VernacDeclareClass _ as x -> xmlTODO ?loc x
-
-  (* Modules and Module Types *)
-  | VernacDeclareModule _ as x -> xmlTODO ?loc x
-  | VernacDefineModule _ as x -> xmlTODO ?loc x
-  | VernacDeclareModuleType _ as x -> xmlTODO ?loc x
-  | VernacInclude _ as x -> xmlTODO ?loc x
-
-  (* Solving *)
-
-  | (VernacSolveExistential _) as x ->
-      xmlLtac ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-  (* Auxiliary file and library management *)
-  | VernacAddLoadPath (recf,name,None) ->
-      xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] []
-  | VernacAddLoadPath (recf,name,Some dp) ->
-      xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name]
-        [PCData (Names.DirPath.to_string dp)]
-  | VernacRemoveLoadPath name -> xmlRemoveLoadPath ?loc ~attr:["path",name] []
-  | VernacAddMLPath (recf,name) ->
-      xmlAddMLPath ?loc ~attr:["rec",string_of_bool recf;"path",name] []
-  | VernacDeclareMLModule sl -> xmlDeclareMLModule ?loc sl
-  | VernacChdir _ as x -> xmlTODO ?loc x
-
-  (* State management *)
-  | VernacWriteState _ as x -> xmlTODO ?loc x
-  | VernacRestoreState _ as x -> xmlTODO ?loc x
-
-  (* Resetting *)
-  | VernacResetName _ as x -> xmlTODO ?loc x
-  | VernacResetInitial as x -> xmlTODO ?loc x
-  | VernacBack _ as x -> xmlTODO ?loc x
-  | VernacBackTo _ -> PCData "VernacBackTo"
-
-  (* Commands *)
-  | VernacCreateHintDb _ as x -> xmlTODO ?loc x
-  | VernacRemoveHints _ as x -> xmlTODO ?loc x
-  | VernacHints _ as x -> xmlTODO ?loc x
-  | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
-      let name = Id.to_string name in
-      let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
-      xmlNotation ?loc attrs name [pp_expr ce]
-  | VernacDeclareImplicits _ as x -> xmlTODO ?loc x
-  | VernacArguments _ as x -> xmlTODO ?loc x
-  | VernacArgumentsScope _ as x -> xmlTODO ?loc x
-  | VernacReserve _ as x -> xmlTODO ?loc x
-  | VernacGeneralizable _ as x -> xmlTODO ?loc x
-  | VernacSetOpacity _ as x -> xmlTODO ?loc x
-  | VernacSetStrategy _ as x -> xmlTODO ?loc x
-  | VernacUnsetOption _ as x -> xmlTODO ?loc x
-  | VernacSetOption _ as x -> xmlTODO ?loc x
-  | VernacSetAppendOption _ as x -> xmlTODO ?loc x
-  | VernacAddOption _ as x -> xmlTODO ?loc x
-  | VernacRemoveOption _ as x -> xmlTODO ?loc x
-  | VernacMemOption _ as x -> xmlTODO ?loc x
-  | VernacPrintOption _ as x -> xmlTODO ?loc x
-  | VernacCheckMayEval (_,_,e) -> xmlCheck ?loc [pp_expr e]
-  | VernacGlobalCheck _ as x -> xmlTODO ?loc x
-  | VernacDeclareReduction _ as x -> xmlTODO ?loc x
-  | VernacPrint _ as x -> xmlTODO ?loc x
-  | VernacSearch _ as x -> xmlTODO ?loc x
-  | VernacLocate _ as x -> xmlTODO ?loc x
-  | VernacRegister _ as x -> xmlTODO ?loc x
-  | VernacComments (cl) ->
-      xmlComment ?loc (List.flatten (List.map pp_comment cl))
-
-  (* Stm backdoor *)
-  | VernacStm _ as x -> xmlTODO ?loc x
-
-  (* Proof management *)
-  | VernacGoal _ as x -> xmlTODO ?loc x
-  | VernacAbort _ as x -> xmlTODO ?loc x
-  | VernacAbortAll -> PCData "VernacAbortAll"
-  | VernacRestart as x -> xmlTODO ?loc x
-  | VernacUndo _ as x -> xmlTODO ?loc x
-  | VernacUndoTo _ as x -> xmlTODO ?loc x
-  | VernacBacktrack _ as x -> xmlTODO ?loc x
-  | VernacFocus _ as x -> xmlTODO ?loc x
-  | VernacUnfocus as x -> xmlTODO ?loc x
-  | VernacUnfocused as x -> xmlTODO ?loc x
-  | VernacBullet _ as x -> xmlTODO ?loc x
-  | VernacSubproof _ as x -> xmlTODO ?loc x
-  | VernacEndSubproof as x -> xmlTODO ?loc x
-  | VernacShow _ as x -> xmlTODO ?loc x
-  | VernacCheckGuard as x -> xmlTODO ?loc x
-  | VernacProof (tac,using) ->
-      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
-
-  (* Toplevel control *)
-  | VernacToplevelControl _ as x -> xmlTODO ?loc x
-
-  (* For extension *)
-  | VernacExtend _ as x ->
-      xmlExtend ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-  (* Flags *)
-  | VernacProgram e -> xmlApply ?loc (Element("program",[],[]) :: [tmpp ?loc e])
-  | VernacLocal (b,e) ->
-      xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) ::
-                    [tmpp ?loc e])
-
-let tmpp ?loc v =
-  match tmpp ?loc v with
-  | Element("ltac",_,_) as x -> x
-  | xml -> xmlGallina ?loc [xml]
diff --git a/ide/texmacspp.mli b/ide/texmacspp.mli
deleted file mode 100644
index c1086a633..000000000
--- a/ide/texmacspp.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-
-val tmpp : ?loc:Loc.t -> vernac_expr -> xml