diff options
| author | herbelin | 2008-09-02 10:06:21 +0000 |
|---|---|---|
| committer | herbelin | 2008-09-02 10:06:21 +0000 |
| commit | 307c7610df6389768848e574170da85f1ab2c8fe (patch) | |
| tree | 656e753eb1fd5c1863385b0d27b552ed7643ca10 /toplevel | |
| parent | 653f63e8b49fd46e686619d8e847e571d8c5442a (diff) | |
Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about
backtracking on coercion classes when a coercion path fails).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11344 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 7ad7c0eda2..f577355d37 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -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 |