diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 23d20dad3..e4331aade 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -234,7 +234,6 @@ let class_of env sigma t = (t, n1, i, u, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in - let t = EConstr.of_constr t in let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) @@ -279,7 +278,6 @@ let apply_on_class_of env sigma t cont = with Not_found -> (* Is it worth to be more incremental on the delta steps? *) let t = Tacred.hnf_constr env sigma t in - let t = EConstr.of_constr t in let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; |