diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-01 14:17:16 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-01 14:17:16 +0000 |
| commit | 03cf2f56231587f98ced95091930696635ef6b50 (patch) | |
| tree | 38707851307300221e6c7616fa44f6d712e85b6c /contrib | |
| parent | e1c8dc453d8a7074925f4c680b98a6b6cc8baf98 (diff) | |
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
Diffstat (limited to 'contrib')
| -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 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) |