diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-09-08 00:15:04 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-09-08 00:15:04 +0200 |
| commit | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch) | |
| tree | c260a140410c796f113584a2f7e6b9b7f6e00aa5 /toplevel | |
| parent | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff) | |
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 2c6a63b0..6ebc663b 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: class.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Pp @@ -139,7 +139,7 @@ let get_source lp source = let (cl1,lv1) = match lp with | [] -> raise Not_found - | t1::_ -> find_class_type t1 + | t1::_ -> find_class_type (Global.env()) Evd.empty t1 in (cl1,lv1,1) | Some cl -> @@ -147,7 +147,7 @@ let get_source lp source = | [] -> raise Not_found | t1::lt -> try - let cl1,lv1 = find_class_type t1 in + let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in if cl = cl1 then cl1,lv1,(List.length lt+1) else raise Not_found with Not_found -> aux lt @@ -157,7 +157,7 @@ let get_target t ind = if (ind > 1) then CL_FUN else - fst (find_class_type t) + fst (find_class_type (Global.env()) Evd.empty t) let prods_of t = let rec aux acc d = match kind_of_term d with @@ -225,8 +225,9 @@ let build_id_coercion idf_opt source = match idf_opt with | Some idf -> idf | None -> + let cl,_ = find_class_type (Global.env()) Evd.empty t in id_of_string ("Id_"^(ident_key_of_class source)^"_"^ - (ident_key_of_class (fst (find_class_type t)))) + (ident_key_of_class cl)) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry |