From 17f92a5a11a70bd4eb0ae3f5108160792167e7bb Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 10 Nov 2004 12:01:52 +0000
Subject: [PATCH] added Baseuri command

---
 helm/ocaml/cic_transformations/tacticAst.ml   | 1 +
 helm/ocaml/cic_transformations/tacticAstPp.ml | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index fd5bde904..7be8293da 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -78,6 +78,7 @@ type thm_flavour =
 
 type 'term command =
   | Abort
+  | Baseuri of string option (** get/set base uri *)
   | Check of 'term
   | Proof
   | Qed of string option
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index f21aca6ba..76f1bbd56 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -89,6 +89,8 @@ let pp_flavour = function
 
 let pp_command = function
   | Abort -> "Abort"
+  | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri
+  | Baseuri None -> "Baseuri"
   | Check term -> sprintf "Check %s" (CicAstPp.pp_term term)
   | Proof -> "Proof"
   | Qed name ->
-- 
2.39.2