Class_tactics API using EConstr.

6 files changed, 29 insertions, 27 deletions

diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index ea9a2b6e1..45ee86c4e 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -62,15 +62,15 @@ TACTIC EXTEND typeclasses_eauto
 END
 
 TACTIC EXTEND head_of_constr
-  [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ]
+  [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND not_evar
-  [ "not_evar" constr(ty) ] -> [ not_evar ty ]
+  [ "not_evar" constr(ty) ] -> [ not_evar (EConstr.of_constr ty) ]
 END
 
 TACTIC EXTEND is_ground
-  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
+  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground (EConstr.of_constr ty)) ]
 END
 
 TACTIC EXTEND autoapply
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index f2ffb0413..a2b6cb97c 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -132,6 +132,7 @@ let find_class_proof proof_type proof_method env evars carrier relation =
   try
     let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in
     let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) (EConstr.of_constr goal) in
+    let c = EConstr.Unsafe.to_constr c in
       if extends_undefined (goalevars evars) evars' then raise Not_found
       else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |]
   with e when Logic.catchable_exception e -> raise Not_found
@@ -1951,6 +1952,7 @@ let default_morphism sign m =
   in
   let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
   let evars, mor = resolve_one_typeclass env (goalevars evars) (EConstr.of_constr morph) in
+  let mor = EConstr.Unsafe.to_constr mor in
     mor, proper_projection mor morph
 
 let add_setoid global binders a aeq t n =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ec36c57e0..e95aba695 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -103,7 +103,7 @@ val is_class_type : evar_map -> EConstr.types -> bool
 
 val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
   ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
-val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> open_constr
+val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr
 
 val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
@@ -120,7 +120,7 @@ val add_instance_hint : global_reference_or_constr -> global_reference list ->
 val remove_instance_hint : global_reference -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
-val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> open_constr) Hook.t
+val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
 val declare_instance : int option -> bool -> global_reference -> unit
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 8ecdd01f2..0ca661557 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,6 +18,7 @@ open Util
 open Names
 open Term
 open Termops
+open EConstr
 open Reduction
 open Proof_type
 open Tacticals
@@ -217,7 +218,6 @@ let auto_unif_flags freeze st =
 }
 
 let e_give_exact flags poly (c,clenv) gl =
-  let open EConstr in
   let (c, _, _) = c in
   let c, gl =
     if poly then
@@ -245,7 +245,6 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
 let unify_resolve_refine poly flags =
-  let open EConstr in
   let open Clenv in
   { enter = begin fun gls ((c, t, ctx),n,clenv) ->
     let env = Proofview.Goal.env gls in
@@ -479,7 +478,8 @@ let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
 
 let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in
-  match kind_of_term ty with
+  let ty = EConstr.of_constr ty in
+  match EConstr.kind sigma ty with
   | Sort (Prop Null) -> true
   | _ -> false
 
@@ -527,22 +527,23 @@ let evars_to_goals p evm =
 let make_resolve_hyp env sigma st flags only_classes pri decl =
   let id = NamedDecl.get_id decl in
   let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
+  let cty = EConstr.of_constr cty in
   let rec iscl env ty =
-    let ctx, ar = decompose_prod_assum ty in
-      match kind_of_term (fst (decompose_app ar)) with
+    let ctx, ar = decompose_prod_assum sigma ty in
+      match EConstr.kind sigma (fst (decompose_app sigma ar)) with
       | Const (c,_) -> is_class (ConstRef c)
       | Ind (i,_) -> is_class (IndRef i)
       | _ ->
           let env' = Environ.push_rel_context ctx env in
-          let ty' = whd_all env' ar in
-               if not (Term.eq_constr ty' ar) then iscl env' ty'
+          let ty' = Reductionops.whd_all env' sigma ar in
+          let ty' = EConstr.of_constr ty' in
+               if not (EConstr.eq_constr sigma ty' ar) then iscl env' ty'
                else false
   in
   let is_class = iscl env cty in
-  let cty = EConstr.of_constr cty in
   let keep = not only_classes || is_class in
     if keep then
-      let c = EConstr.mkVar id in
+      let c = mkVar id in
       let name = PathHints [VarRef id] in
       let hints =
         if is_class then
@@ -1466,6 +1467,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
   let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
+  let (ev, _) = destEvar sigma t in
   let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
   let st = Hint_db.transparent_state hints in
@@ -1480,11 +1482,9 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
       with Refiner.FailError _ -> raise Not_found
   in
   let evd = sig_sig gls' in
-  let t = EConstr.Unsafe.to_constr t in
-  let t' = let (ev, inst) = destEvar t in
-    mkEvar (ev, Array.map_of_list EConstr.Unsafe.to_constr subst)
-  in
-  let term = Evarutil.nf_evar evd t' in
+  let t' = mkEvar (ev, Array.of_list subst) in
+  let term = Evarutil.nf_evar evd (EConstr.Unsafe.to_constr t') in
+  let term = EConstr.of_constr term in
     evd, term
 
 let _ =
@@ -1495,8 +1495,9 @@ let _ =
     Used in the partial application tactic. *)
 
 let rec head_of_constr sigma t =
-  let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma (EConstr.of_constr t))) in
-    match kind_of_term t with
+  let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma t)) in
+  let t = EConstr.of_constr t in
+    match EConstr.kind sigma t with
     | Prod (_,_,c2)  -> head_of_constr sigma c2
     | LetIn (_,_,_,c2) -> head_of_constr sigma c2
     | App (f,args)  -> head_of_constr sigma f
@@ -1505,17 +1506,16 @@ let rec head_of_constr sigma t =
 let head_of_constr h c =
   Proofview.tclEVARMAP >>= fun sigma ->
   let c = head_of_constr sigma c in
-  let c = EConstr.of_constr c in
   letin_tac None (Name h) c None Locusops.allHyps
 
 let not_evar c =
   Proofview.tclEVARMAP >>= fun sigma ->
-  match Evarutil.kind_of_term_upto sigma c with
+  match EConstr.kind sigma c with
   | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
   | _ -> Proofview.tclUNIT ()
 
 let is_ground c gl =
-  if Evarutil.is_ground_term (project gl) (EConstr.of_constr c) then tclIDTAC gl
+  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
   else tclFAIL 0 (str"Not ground") gl
 
 let autoapply c i gl =
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 027b7dcd7..171b5c4ea 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -10,6 +10,7 @@
 
 open Names
 open Constr
+open EConstr
 open Tacmach
 
 val catchable : exn -> bool
@@ -24,13 +25,13 @@ val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
                         depth:(Int.t option) ->
                         Hints.hint_db_name list -> unit Proofview.tactic
 
-val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic
+val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
 val not_evar : constr -> unit Proofview.tactic
 
 val is_ground : constr -> tactic
 
-val autoapply : EConstr.constr -> Hints.hint_db_name -> tactic
+val autoapply : constr -> Hints.hint_db_name -> tactic
 
 module Search : sig
   val eauto_tac :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59ffd8b62..c025ca9b5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1734,7 +1734,6 @@ let solve_remaining_apply_goals =
       let concl = EConstr.of_constr concl in
       if Typeclasses.is_class_type evd concl then
         let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in
-        let c' = EConstr.of_constr c' in
         let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in
         Sigma.Unsafe.of_pair (tac, evd')
 	else Sigma.here (Proofview.tclUNIT ()) sigma