diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/xml/proofTree2Xml.ml4 | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/xml/proofTree2Xml.ml4')
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 05be01bc..a501fb6a 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 @@ -91,6 +90,7 @@ let string_of_prim_rule x = match x with | Proof_type.Thin _ -> "Thin" | Proof_type.ThinBody _-> "ThinBody" | Proof_type.Move (_,_,_) -> "Move" + | Proof_type.Order _ -> "Order" | Proof_type.Rename (_,_) -> "Rename" | Proof_type.Change_evars -> "Change_evars" |