From 693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 25 Jun 2008 18:19:21 +0000
Subject: Création du fichier dumpglob.ml, qui rassemble les fonctions de
 globalisation (add_glob* et dump_*)

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

(limited to 'toplevel/classes.ml')

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 30fee26a03..d07051b718 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -447,7 +447,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 		  try 
 		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
 		    let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		      Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
+		      Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		      c :: props, rest'
 		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
 		([], props) k.cl_props
-- 
cgit v1.2.3