Classops API using EConstr.

5 files changed, 23 insertions, 23 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 88ae4695b8..d264a19047 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -585,7 +585,7 @@ let scope_class_compare : scope_class -> scope_class -> int =
   cl_typ_ord
 
 let compute_scope_class t =
-  let (cl,_,_) = find_class_type Evd.empty t in
+  let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in
   cl
 
 module ScopeClassOrd =
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 =
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