diff options
| author | barras | 2001-05-03 09:54:17 +0000 |
|---|---|---|
| committer | barras | 2001-05-03 09:54:17 +0000 |
| commit | bf352b0b29a8e3d55eaa986c4f493af48f8ddf52 (patch) | |
| tree | b0633f3a1ee73bd685327c2c988426d65de7a58a /contrib/xml/xmlcommand.ml | |
| parent | c4a517927f148e0162d22cb7077fa0676d799926 (diff) | |
Changement de la structure des points fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 3927827276..573f4319b3 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -446,7 +446,7 @@ let print_term inner_types l env csr = ) a [<>] >] ) - | T.IsFix ((ai,i),((t,f,b) as rec_decl)) -> + | T.IsFix ((ai,i),((f,t,b) as rec_decl)) -> X.xml_nempty "FIX" (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) (force @@ -458,7 +458,7 @@ let print_term inner_types l env csr = [< term_display idradix false l env ti >] ; X.xml_nempty "body" [] [< term_display idradix false - ((List.rev f)@l) + ((Array.to_list f)@l) (E.push_rec_types rec_decl env) bi >] @@ -466,11 +466,11 @@ let print_term inner_types l env csr = i >] ) - (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) (Array.of_list f) ) + (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) f ) [<>] >] ) - | T.IsCoFix (i,((t,f,b) as rec_decl)) -> + | T.IsCoFix (i,((f,t,b) as rec_decl)) -> X.xml_nempty "COFIX" (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) (force @@ -481,7 +481,7 @@ let print_term inner_types l env csr = [< term_display idradix false l env ti >] ; X.xml_nempty "body" [] [< term_display idradix false - ((List.rev f)@l) + ((Array.to_list f)@l) (E.push_rec_types rec_decl env) bi >] @@ -489,7 +489,7 @@ let print_term inner_types l env csr = i >] ) - (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) (Array.of_list f) ) [<>] + (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) f ) [<>] >] ) | T.IsEvar _ -> |