From 047037ecc6494efa77bde400bdf5e77b16daa5e0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 13 Sep 2008 19:01:08 +0000
Subject: Remove redefinition of id in Program.Basics, just add maximal
 implicits.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11401 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f5b0355f5a..ba090c5336 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -557,7 +557,7 @@ let iff = lazy (gen_constant ["Init"; "Logic"] "iff")
 let coq_all = lazy (gen_constant ["Init"; "Logic"] "all")
 let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
 let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
-let coq_id = lazy (gen_constant ["Program"; "Basics"] "id")
+let coq_id = lazy (gen_constant ["Init"; "Datatypes"] "id")
 
 let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive")
 let reflexive_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "reflexivity")
-- 
cgit v1.2.3