diff options
| author | Pierre-Marie Pédrot | 2016-11-07 19:07:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:20 +0100 |
| commit | ce2b509734f3b70494a0a35b0b4eda593c1c8eb6 (patch) | |
| tree | 77e87e5da2b453e9ae918eef039b6511d3612597 /toplevel | |
| parent | 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 (diff) | |
Classops API using EConstr.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 86fd4d9a20..6295eb3361 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -120,7 +120,7 @@ let get_source lp source = let (cl1,u1,lv1) = match lp with | [] -> raise Not_found - | t1::_ -> find_class_type Evd.empty t1 + | t1::_ -> find_class_type Evd.empty (EConstr.of_constr t1) in (cl1,u1,lv1,1) | Some cl -> @@ -128,7 +128,7 @@ let get_source lp source = | [] -> raise Not_found | t1::lt -> try - let cl1,u1,lv1 = find_class_type Evd.empty t1 in + let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1) else raise Not_found with Not_found -> aux lt @@ -138,7 +138,7 @@ let get_target t ind = if (ind > 1) then CL_FUN else - match pi1 (find_class_type Evd.empty t) with + match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with | CL_CONST p when Environ.is_projection p (Global.env ()) -> CL_PROJ p | x -> x @@ -215,7 +215,7 @@ let build_id_coercion idf_opt source poly = match idf_opt with | Some idf -> idf | None -> - let cl,u,_ = find_class_type sigma t in + let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in |