From fd623567d78e917ccc08995b14b1c66eb419487e Mon Sep 17 00:00:00 2001 From: sacerdot Date: Thu, 1 Apr 2004 16:48:15 +0000 Subject: LocalFact added as a choice for the "as" attribute of ht:VARIABLE in the DTD. Used for local proofs (e.g. "Let x : True. auto. Qed."). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5630 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/xmlcommand.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index ad5d4d4a6..8e3d7cc35 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -19,7 +19,7 @@ (* CONFIGURATION PARAMETERS *) -let verbose = ref true;; +let verbose = ref false;; (* HOOKS *) let print_proof_tree, set_print_proof_tree = @@ -461,7 +461,7 @@ let kind_of_variable id = | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture" | DK.IsDefinition -> "VARIABLE","LocalDefinition" | DK.IsConjecture -> "VARIABLE","Conjecture" - | DK.IsProof DK.LocalStatement -> "VARIABLE","Hypothesis" + | DK.IsProof DK.LocalStatement -> "VARIABLE","LocalFact" ;; let kind_of_constant kn = @@ -570,7 +570,7 @@ let show_pftreestate internal fn (kind,pftst) id = let uri = "cic:/" ^ String.concat "/" (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.Variable) in - let kind_of_var = "VARIABLE","Hypothesis" in + let kind_of_var = "VARIABLE","LocalFact" in if not internal then print_object_kind uri kind_of_var; uri | Decl_kinds.IsGlobal _ -> -- cgit v1.2.3