diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-01 16:48:15 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-01 16:48:15 +0000 |
| commit | fd623567d78e917ccc08995b14b1c66eb419487e (patch) | |
| tree | 3a77218334353cb48fa5331ce90a05df624e2d02 | |
| parent | 696880386882044f4ef5529f50f8815eac671ace (diff) | |
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
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 6 |
1 files 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 _ -> |