diff options
| author | herbelin | 2009-01-14 12:54:59 +0000 |
|---|---|---|
| committer | herbelin | 2009-01-14 12:54:59 +0000 |
| commit | 511cb2f5f42d80af9262b5cf7458a434cd652e95 (patch) | |
| tree | 1ea8c93c8dc668079fedfc32eb7df6696fa51c30 /contrib/xml/proofTree2Xml.ml4 | |
| parent | 7aea5b4a925f752c8e056d2ca1e9bfe48a066372 (diff) | |
Fixing #1960 (xml bug with external on goal variable) and #1961
(anomaly while parsing $ not followed by an ident).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11785 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/proofTree2Xml.ml4')
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 26b1b0b760..a501fb6a63 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -31,7 +31,6 @@ let constr_to_xml obj sigma env = let ids_to_inner_sorts = Hashtbl.create 503 in let ids_to_inner_types = Hashtbl.create 503 in - let pvars = [] in (* named_context holds section variables and local variables *) let named_context = Environ.named_context env in (* real_named_context holds only the section variables *) @@ -54,7 +53,7 @@ let constr_to_xml obj sigma env = try let annobj = Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids - ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars rel_env + ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env idrefs sigma (Unshare.unshare obj') None in Acic2Xml.print_term ids_to_inner_sorts annobj |