diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 18:10:57 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 18:10:57 +0000 |
| commit | 1f96d480842a1206a9334d0c8b1b6cc4647066ef (patch) | |
| tree | 9fc22a20d49bcefca1d863aee9d36c5fab03334f /contrib/xml | |
| parent | 6c7f6fa6c215e5e28fcf23bf28ccb9db543709ba (diff) | |
Transparent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 3116bd49b..f4b75583c 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -847,7 +847,7 @@ let print_object lobj id sp dn fv env = let hyps = string_list_of_named_context_list hyps in print_mutual_inductive packs fv hyps env inner_types | "VARIABLE" -> - let (_,(varentry,_,_)) = Declare.out_variable lobj in + let (_,(varentry,_)) = Declare.out_variable lobj in begin match varentry with Declare.SectionLocalDef body -> |