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 ++--
 contrib/subtac/g_subtac.ml4 | 9 +++++----
 2 files changed, 7 insertions(+), 6 deletions(-)

(limited to 'contrib')

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 ->
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index b7cb7fb233..46bc1a0b86 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -53,7 +53,7 @@ open Constr
 let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 GEXTEND Gram
-  GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder_let Constr.binder subtac_nameopt;
+  GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt;
  
   subtac_gallina_loc:
     [ [ g = Vernac.gallina -> loc, g
@@ -66,9 +66,9 @@ GEXTEND Gram
     ;
 
   Constr.binder_let:
-    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> 
+    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-	    LocalRawAssum ([id], default_binder_kind, typ)
+          [LocalRawAssum ([id], default_binder_kind, typ)]
     ] ];
 
   Constr.binder:
@@ -141,7 +141,8 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
 VERNAC COMMAND EXTEND Subtac_Set_Solver
 | [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ 
     Coqlib.check_required_library ["Coq";"Program";"Tactics"];
-    Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ]
+    Tacinterp.add_tacdef false 
+      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
-- 
cgit v1.2.3