From 03cf2f56231587f98ced95091930696635ef6b50 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Fri, 1 Dec 2000 14:17:16 +0000 Subject: LETIN now has a letintarget instead of a target git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1042 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/xmlcommand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'contrib/xml') diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 5c5b3e5f4..3e52f311d 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -309,7 +309,7 @@ let print_term inner_types l env csr = X.xml_nempty "LETIN" (add_sort_attribute true ["id", next_id]) (force [< X.xml_nempty "term" [] (term_display idradix false l env s) ; - X.xml_nempty "target" ["binder",(N.string_of_id nid')] + X.xml_nempty "letintarget" ["binder",(N.string_of_id nid')] (term_display idradix false ((N.Name nid')::l) (E.push_rel_def (N.Name nid', s, t) env) -- cgit v1.2.3