Classops API using EConstr.

3 files changed, 18 insertions, 18 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 577f41a7d7..753127357a 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -193,7 +193,7 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab
 
 let find_class_type sigma t =
   let inj = EConstr.Unsafe.to_constr in
-  let t', args = Reductionops.whd_betaiotazeta_stack sigma (EConstr.of_constr t) in
+  let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
   match EConstr.kind sigma t' with
     | Var id -> CL_SECVAR id, Univ.Instance.empty, List.map inj args
     | Const (sp,u) -> CL_CONST sp, u, List.map inj args
@@ -215,7 +215,7 @@ let subst_cl_typ subst ct = match ct with
   | CL_CONST c ->
       let c',t = subst_con_kn subst c in
 	if c' == c then ct else
-         pi1 (find_class_type Evd.empty t)
+         pi1 (find_class_type Evd.empty (EConstr.of_constr t))
   | CL_IND i ->
       let i' = subst_ind subst i in
 	if i' == i then ct else CL_IND i'
@@ -231,10 +231,10 @@ let class_of env sigma t =
     try
       let (cl, u, args) = find_class_type sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
-      (t, n1, i, u, args)
+      (EConstr.Unsafe.to_constr t, n1, i, u, args)
     with Not_found ->
-      let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in
-      let (cl, u, args) = find_class_type sigma t in
+      let t = Tacred.hnf_constr env sigma t in
+      let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, u, args)
   in
@@ -274,11 +274,11 @@ let apply_on_class_of env sigma t cont =
     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;
-    t, cont i
+    EConstr.Unsafe.to_constr t, cont i
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
-    let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in
-    let (cl, u, args) = find_class_type sigma t in
+    let t = Tacred.hnf_constr env sigma t in
+    let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in
     let (i, { cl_param = n1 } ) = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
     t, cont i
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index d509739cf4..4b8a2c1c07 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -59,15 +59,15 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
 (** [find_class_type env sigma c] returns the head reference of [c],
     its universe instance and its arguments *)
-val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list
+val find_class_type : evar_map -> EConstr.types -> cl_typ * Univ.universe_instance * constr list
 
 (** raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> types -> types * cl_index
+val class_of : env -> evar_map -> EConstr.types -> types * cl_index
 
 (** raises [Not_found] if not mapped to a class *)
 val inductive_class_of : inductive -> cl_index
 
-val class_args_of : env -> evar_map -> types -> constr list
+val class_args_of : env -> evar_map -> EConstr.types -> constr list
 
 (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
 val declare_coercion :
@@ -84,11 +84,11 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer
 (** @raise Not_found in the following functions when no path exists *)
 
 val lookup_path_between_class : cl_index * cl_index -> inheritance_path
-val lookup_path_between : env -> evar_map -> types * types ->
+val lookup_path_between : env -> evar_map -> EConstr.types * EConstr.types ->
       types * types * inheritance_path
-val lookup_path_to_fun_from : env -> evar_map -> types ->
+val lookup_path_to_fun_from : env -> evar_map -> EConstr.types ->
       types * inheritance_path
-val lookup_path_to_sort_from : env -> evar_map -> types ->
+val lookup_path_to_sort_from : env -> evar_map -> EConstr.types ->
       types * inheritance_path
 val lookup_pattern_path_between :
   env -> inductive * inductive -> (constructor * int) list
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 04e235cc53..90cd3b60b9 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -358,7 +358,7 @@ let apply_coercion env sigma p hj typ_cl =
         (fun (ja,typ_cl,sigma) i ->
 	  let ((fv,isid,isproj),ctx) = coercion_value i in
 	  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-	  let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
+	  let argl = (class_args_of env sigma (EConstr.of_constr typ_cl))@[ja.uj_val] in
 	  let sigma, jres = 
 	    apply_coercion_args env sigma true isproj argl fv 
 	  in
@@ -382,7 +382,7 @@ let inh_app_fun_core env evd j =
 	  (evd',{ uj_val = j.uj_val; uj_type = EConstr.Unsafe.to_constr t })
     | _ ->
       	try let t,p =
-	  lookup_path_to_fun_from env evd j.uj_type in
+	  lookup_path_to_fun_from env evd (EConstr.of_constr j.uj_type) in
 	    apply_coercion env evd p j t
 	with Not_found | NoCoercion ->
           if Flags.is_program_mode () then
@@ -407,7 +407,7 @@ let inh_app_fun resolve_tc env evd j =
 
 let inh_tosort_force loc env evd j =
   try
-    let t,p = lookup_path_to_sort_from env evd j.uj_type in
+    let t,p = lookup_path_to_sort_from env evd (EConstr.of_constr j.uj_type) in
     let evd,j1 = apply_coercion env evd p j t in
     let j2 = on_judgment_type (whd_evar evd) j1 in
       (evd,type_judgment env j2)
@@ -448,7 +448,7 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
   else
     let evd, v', t' =
       try
-	let t2,t1,p = lookup_path_between env evd (t,c1) in
+	let t2,t1,p = lookup_path_between env evd (EConstr.of_constr t,EConstr.of_constr c1) in
 	  match v with
 	  | Some v ->
 	    let evd,j =