From 30443ddaba7a0cc996216b3d692b97e0b05907fe Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 11 May 2008 22:04:26 +0000
Subject: - Cleanup parsing of binders, reducing to a single production for all
   binders. - Change syntax of type class instances to better match the usual
 syntax of   lemmas/definitions with name first, then arguments ":" instance. 
  Update theories/Classes accordingly. - Correct globalization of tactic
 references when doing Ltac :=/::=, update   documentation. - Remove the not
 so useful "(x &)" and "{{x}}" syntaxes from   Program.Utils, and subset_scope
 as well.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9f7491d5f4..9db1c7dc42 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1609,8 +1609,8 @@ let rec xlate_vernac =
    | VernacDeclareTacticDefinition (true, tacs) ->
        (match List.map 
 	 (function
-	      ((_, id), _, body) ->
-		CT_tac_def(CT_ident (string_of_id id), xlate_tactic body))
+	      (id, _, body) ->
+		CT_tac_def(reference_to_ct_ID id, xlate_tactic body))
 	 tacs with
 	     [] -> assert false
 	   | fst::tacs1 ->
-- 
cgit v1.2.3