From bc9cc53fbb0cb8676106e0c4d74053bbe1ac1a8e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Jun 2005 15:48:01 +0000
Subject: [PATCH] misc -> domMisc

---
 helm/ocaml/cic_transformations/.depend                   | 8 ++++----
 helm/ocaml/cic_transformations/Makefile                  | 2 +-
 helm/ocaml/cic_transformations/applyTransformation.ml    | 4 ++--
 helm/ocaml/cic_transformations/{misc.ml => domMisc.ml}   | 0
 helm/ocaml/cic_transformations/{misc.mli => domMisc.mli} | 0
 helm/ocaml/cic_transformations/tacticAst.ml              | 1 +
 helm/ocaml/cic_transformations/tacticAstPp.ml            | 1 +
 7 files changed, 9 insertions(+), 7 deletions(-)
 rename helm/ocaml/cic_transformations/{misc.ml => domMisc.ml} (100%)
 rename helm/ocaml/cic_transformations/{misc.mli => domMisc.mli} (100%)

diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend
index b05f4e1ad..4203ff228 100644
--- a/helm/ocaml/cic_transformations/.depend
+++ b/helm/ocaml/cic_transformations/.depend
@@ -35,16 +35,16 @@ sequent2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \
     sequent2pres.cmi 
 sequent2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \
     sequent2pres.cmi 
-misc.cmo: misc.cmi 
-misc.cmx: misc.cmi 
+domMisc.cmo: domMisc.cmi 
+domMisc.cmx: domMisc.cmi 
 xml2Gdome.cmo: xml2Gdome.cmi 
 xml2Gdome.cmx: xml2Gdome.cmi 
 sequentPp.cmo: cic2Xml.cmi sequentPp.cmi 
 sequentPp.cmx: cic2Xml.cmx sequentPp.cmi 
 applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi mpresentation.cmi \
-    misc.cmi content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi 
+    content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi 
 applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx mpresentation.cmx \
-    misc.cmx content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi 
+    content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi 
 tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi 
 tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi 
 boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi 
diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile
index 3c43c338d..4675291d4 100644
--- a/helm/ocaml/cic_transformations/Makefile
+++ b/helm/ocaml/cic_transformations/Makefile
@@ -14,7 +14,7 @@ INTERFACE_FILES = \
 	acic2Ast.mli \
 	cicAstPp.mli ast2pres.mli content2pres.mli \
 	sequent2pres.mli \
-	misc.mli xml2Gdome.mli sequentPp.mli \
+	domMisc.mli xml2Gdome.mli sequentPp.mli \
 	applyTransformation.mli \
 	tacticAstPp.mli boxPp.mli tacticAst2Box.mli
 IMPLEMENTATION_FILES = \
diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml
index 57d26f168..560f6a0d1 100644
--- a/helm/ocaml/cic_transformations/applyTransformation.ml
+++ b/helm/ocaml/cic_transformations/applyTransformation.ml
@@ -45,7 +45,7 @@ let mml_of_cic_sequent metasenv sequent =
   let pres_sequent = 
     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
   let xmlpres = mpres_document pres_sequent in
-  Xml2Gdome.document_of_xml Misc.domImpl xmlpres,
+  Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
    (asequent,
     (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))
 
@@ -60,7 +60,7 @@ let mml_of_cic_object obj =
   in
   let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
   let xmlpres = mpres_document pres in
-  let mathml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in
+  let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in
   (mathml,(annobj,
    (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
   ids_to_inner_sorts,ids_to_inner_types)))
diff --git a/helm/ocaml/cic_transformations/misc.ml b/helm/ocaml/cic_transformations/domMisc.ml
similarity index 100%
rename from helm/ocaml/cic_transformations/misc.ml
rename to helm/ocaml/cic_transformations/domMisc.ml
diff --git a/helm/ocaml/cic_transformations/misc.mli b/helm/ocaml/cic_transformations/domMisc.mli
similarity index 100%
rename from helm/ocaml/cic_transformations/misc.mli
rename to helm/ocaml/cic_transformations/domMisc.mli
diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 1525cfd8b..191323599 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -128,6 +128,7 @@ type obj =
 
 type ('term,'obj) command =
   | Set of loc * string * string
+  | Drop of loc
   | Qed of loc
       (** name.
        * Name is needed when theorem was started without providing a name
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index bc4346e91..ee099e420 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -220,6 +220,7 @@ let pp_obj = function
 
 let pp_command = function
   | Qed _ -> "qed"
+  | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
   | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
   | Alias (_,s) -> pp_alias s
-- 
2.39.2