Refine API using EConstr.

11 files changed, 53 insertions, 32 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index bc55ac458..7ccf9d810 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -719,6 +719,7 @@ let undefined_evars_of_evar_info evd evi =
    [evar_map]. If unification only need to check superficially, tactics
    do not have this luxury, and need the more complete version. *)
 let occur_evar_upto sigma n c =
+  let c = EConstr.Unsafe.to_constr c in
   let rec occur_rec c = match kind_of_term c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
     | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 8f3c3c352..431d98083 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -128,7 +128,7 @@ val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 (** [occur_evar_upto sigma k c] returns [true] if [k] appears in
     [c]. It looks up recursively in [sigma] for the value of existential
     variables. *)
-val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
+val occur_evar_upto : evar_map -> Evar.t -> EConstr.t -> bool
 
 (** {6 Value/Type constraints} *)
 
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 981ff549d..c3ca8f906 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -353,7 +353,10 @@ let refine_tac ist simple c =
     let flags = constr_flags in
     let expected_type = Pretyping.OfType (EConstr.of_constr concl) in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
-    let update = { run = fun sigma -> c.delayed env sigma } in
+    let update = { run = fun sigma ->
+      let Sigma (c, sigma, p) = c.delayed env sigma in
+      Sigma (EConstr.of_constr c, sigma, p)
+    } in
     let refine = Refine.refine ~unsafe:true update in
     if simple then refine
     else refine <*>
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 4d65b4c69..dfcfbfbd3 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1556,7 +1556,7 @@ let assert_replacing id newt tac =
         if Id.equal n id then ev' else mkVar n
       in
       let (e, _) = destEvar ev in
-      Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
+      Sigma (EConstr.of_constr (mkEvar (e, Array.map_of_list map nc)), sigma, p +> q)
     end }
   end } in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
@@ -1582,7 +1582,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	match clause, prf with
 	| Some id, Some p ->
             let tac = tclTHENLIST [
-              Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h };
+              Refine.refine ~unsafe:false { run = fun h -> Sigma.here (EConstr.of_constr p) h };
               Proofview.Unsafe.tclNEWGOALS gls;
             ] in
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1597,7 +1597,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             let env = Proofview.Goal.env gl in
             let make = { run = begin fun sigma ->
               let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in
-              Sigma (mkApp (p, [| ev |]), sigma, q)
+              Sigma (EConstr.of_constr (mkApp (p, [| ev |])), sigma, q)
             end } in
             Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
             end }
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4c598ca29..7499bc251 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -86,12 +86,11 @@ module V82 = struct
   (* Instantiates a goal with an open term *)
   let partial_solution sigma evk c =
     (* Check that the goal itself does not appear in the refined term *)
-    let c = EConstr.Unsafe.to_constr c in
     let _ =
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
-      else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c)
+      else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
     in
-    Evd.define evk c sigma
+    Evd.define evk (EConstr.Unsafe.to_constr c) sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 067764c00..11eabe0a9 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -47,7 +47,7 @@ let typecheck_evar ev env sigma =
 
 let typecheck_proof c concl env sigma =
   let evdref = ref sigma in
-  let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in
+  let () = Typing.e_check env evdref c concl in
   !evdref
 
 let (pr_constrv,pr_constr) =
@@ -77,6 +77,7 @@ let make_refine_enter ?(unsafe = true) f =
   let sigma = Sigma.to_evar_map sigma in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
+  let concl = EConstr.of_constr concl in
   (** Save the [future_goals] state to restore them after the
       refinement. *)
   let prev_future_goals = Evd.future_goals sigma in
@@ -98,9 +99,10 @@ let make_refine_enter ?(unsafe = true) f =
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
-    else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c)
+    else Pretype_errors.error_occur_check env sigma self c
   in
   (** Proceed to the refinement *)
+  let c = EConstr.Unsafe.to_constr c in
   let sigma = match evkmain with
     | None -> Evd.define self c sigma
     | Some evk ->
@@ -133,23 +135,22 @@ let refine ?(unsafe = true) f =
 (** Useful definitions *)
 
 let with_type env evd c t =
-  let c = EConstr.of_constr c in
   let my_type = Retyping.get_type_of env evd c in
   let my_type = EConstr.of_constr my_type in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
-    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t)
+    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
   in
   evd , j'.Environ.uj_val
 
 let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
   let gl = Proofview.Goal.assume gl in
   let concl = Proofview.Goal.concl gl in
+  let concl = EConstr.of_constr concl in
   let env = Proofview.Goal.env gl in
   let f = { run = fun h ->
     let Sigma (c, h, p) = f.run h in
     let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
-    let c = EConstr.Unsafe.to_constr c in
     Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
   } in
   refine ?unsafe f
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 4158e446c..205b97974 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,7 +21,7 @@ val pr_constr :
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
 (** In [refine ?unsafe t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
@@ -30,16 +30,16 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [unsafe] is [false] (default is [true]) [t] is
     type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
 (** A generalization of [refine] which assumes exactly one goal under focus *)
 
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
-  Term.constr -> Term.types -> Evd.evar_map * EConstr.constr
+  EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index be8d7eaa5..b0f355170 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -269,7 +269,7 @@ let unify_resolve_refine poly flags =
             {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
             concl;
         !evdref
-      in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
+      in Sigma.here (EConstr.of_constr term) (Sigma.Unsafe.of_evar_map sigma') }
   end }
 
 (** Dealing with goals of the form A -> B and hints of the form
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 9324d8e37..eebc67222 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -458,6 +458,7 @@ let raw_inversion inv_kind id status names =
     in
     let refined id =
       let prf = mkApp (mkVar id, args) in
+      let prf = EConstr.of_constr prf in
       Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
     in
     let neqns = List.length realargs in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index eebb2a038..639a12b34 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -177,7 +177,7 @@ let unsafe_intro env store decl b =
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
     let Sigma (ev, sigma, p) = new_evar_instance nctx sigma (EConstr.of_constr nb) ~principal:true ~store ninst in
-    Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p)
+    Sigma (EConstr.of_constr (mkNamedLambda_or_LetIn decl ev), sigma, p)
   end }
 
 let introduction ?(check=true) id =
@@ -218,7 +218,7 @@ let convert_concl ?(check=true) ty k =
         end else Sigma.here () sigma in
       let Sigma (x, sigma, q) = Evarutil.new_evar env sigma ~principal:true ~store ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
-      Sigma (ans, sigma, p +> q)
+      Sigma (EConstr.of_constr ans, sigma, p +> q)
     end }
   end }
 
@@ -231,7 +231,8 @@ let convert_hyp ?(check=true) d =
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
     Refine.refine ~unsafe:true { run = begin fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr ty)
+      let Sigma (c, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr ty) in
+      Sigma (EConstr.of_constr c, sigma, p)
     end }
   end }
 
@@ -301,7 +302,8 @@ let clear_gen fail = function
     in
     let env = reset_with_named_context hyps env in
     let tac = Refine.refine ~unsafe:true { run = fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr concl)
+      let Sigma (c, sigma, p) = Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr concl) in
+      Sigma (EConstr.of_constr c, sigma, p)
     } in
     Sigma.Unsafe.of_pair (tac, !evdref)
   end }
@@ -331,7 +333,8 @@ let move_hyp id dest =
     let sign' = move_hyp_in_named_context sigma id dest sign in
     let env = reset_with_named_context sign' env in
     Refine.refine ~unsafe:true { run = begin fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr ty)
+      let Sigma (c, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr ty) in
+      Sigma (EConstr.of_constr c, sigma, p)
     end }
   end }
 
@@ -385,7 +388,8 @@ let rename_hyp repl =
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~unsafe:true { run = begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma (EConstr.of_constr nconcl) ~principal:true ~store instance
+        let Sigma (c, sigma, p) = Evarutil.new_evar_instance nctx sigma (EConstr.of_constr nconcl) ~principal:true ~store instance in
+        Sigma (EConstr.of_constr c, sigma, p)
       end }
     end }
 
@@ -541,6 +545,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
     let typarray = Array.of_list (List.map pi3 all) in
     let bodies = Array.of_list evs in
     let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
+    let oterm = EConstr.of_constr oterm in
     Sigma (oterm, sigma, p)
   end }
 end }
@@ -592,6 +597,7 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
     let typarray = Array.of_list types in
     let bodies = Array.of_list evs in
     let oterm = Term.mkCoFix (0, (funnames, typarray, bodies)) in
+    let oterm = EConstr.of_constr oterm in
     Sigma (oterm, sigma, p)
   end }
 end }
@@ -1248,6 +1254,7 @@ let cut c =
         let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (EConstr.of_constr (mkArrow c (Vars.lift 1 concl))) in
         let Sigma (x, h, q) = Evarutil.new_evar env h (EConstr.of_constr c) in
         let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
+        let f = EConstr.of_constr f in
         Sigma (f, h, p +> q)
       end }
     else
@@ -1680,6 +1687,7 @@ 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
@@ -1921,6 +1929,7 @@ let cut_and_apply c =
           let Sigma (f, sigma, p) = Evarutil.new_evar env sigma (EConstr.of_constr typ) in
           let Sigma (x, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr c1) in
           let ans = mkApp (f, [|mkApp (c, [|x|])|]) in
+          let ans = EConstr.of_constr ans in
           Sigma (ans, sigma, p +> q)
         end }
       | _ -> error "lapply needs a non-dependent product."
@@ -1937,6 +1946,7 @@ let cut_and_apply c =
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
 let exact_no_check c =
+  let c = EConstr.of_constr c in
   Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
 
 let exact_check c =
@@ -1968,6 +1978,7 @@ let exact_proof c =
   Refine.refine { run = begin fun sigma ->
     let sigma = Sigma.to_evar_map sigma in
     let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in
+    let c = EConstr.of_constr c in
     let sigma = Evd.merge_universe_context sigma ctx in
     Sigma.Unsafe.of_pair (c, sigma)
   end }
@@ -2083,7 +2094,8 @@ let clear_body ids =
     in
     check <*>
     Refine.refine ~unsafe:true { run = begin fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr concl)
+      let Sigma (c, sigma, p) = Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr concl) in
+      Sigma (EConstr.of_constr c, sigma, p)
     end }
   end }
 
@@ -2137,7 +2149,7 @@ let apply_type newcl args =
       let newcl = nf_betaiota (Sigma.to_evar_map sigma) (EConstr.of_constr newcl) (* As in former Logic.refine *) in
       let Sigma (ev, sigma, p) =
         Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr newcl) in
-      Sigma (applist (ev, args), sigma, p)
+      Sigma (EConstr.of_constr (applist (ev, args)), sigma, p)
     end }
   end }
 
@@ -2157,7 +2169,7 @@ let bring_hyps hyps =
       Refine.refine { run = begin fun sigma ->
         let Sigma (ev, sigma, p) =
           Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr newcl) in
-        Sigma (mkApp (ev, args), sigma, p)
+        Sigma (EConstr.of_constr (mkApp (ev, args)), sigma, p)
       end }
     end }
 
@@ -2683,11 +2695,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let refl = applist (refl, [t;mkVar id]) in
       let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
       let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store (EConstr.of_constr ccl) in
-      Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r)
+      Sigma (EConstr.of_constr (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x)), sigma, p +> q +> r)
   | None ->
       let newenv = insert_before [decl] lastlhyp env in
       let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store (EConstr.of_constr ccl) in
-      Sigma (mkNamedLetIn id c t x, sigma, p)
+      Sigma (EConstr.of_constr (mkNamedLetIn id c t x), sigma, p)
 
 let letin_tac with_eq id c ty occs =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
@@ -2875,7 +2887,7 @@ let new_generalize_gen_let lconstr =
     let tac =
 	Refine.refine { run = begin fun sigma ->
           let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr newcl) in
-          Sigma ((applist (ev, args)), sigma, p)
+          Sigma (EConstr.of_constr (applist (ev, args)), sigma, p)
 	end }
     in
     Sigma.Unsafe.of_pair (tac, sigma)
@@ -3569,7 +3581,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
     (* Apply the reflexivity proofs on the indices. *)
   let appeqs = mkApp (instc, Array.of_list refls) in
     (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
-  Sigma (mkApp (appeqs, abshypt), sigma, p)
+  Sigma (EConstr.of_constr (mkApp (appeqs, abshypt)), sigma, p)
   end }
 
 let hyps_of_vars env sigma sign nogen hyps =
@@ -5005,6 +5017,10 @@ module New = struct
       {onhyps=None; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
+    let c = { run = begin fun sigma ->
+      let Sigma (c, sigma, p) = c.run sigma in
+      Sigma (EConstr.of_constr c, sigma, p)
+    end } in
     Refine.refine ?unsafe c <*>
     reduce_after_refine
 end
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1055d28b6..7c4ad6225 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -332,7 +332,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
+                      Refine.refine { run = fun evm -> Sigma (EConstr.of_constr (Option.get term), evm, Sigma.refl) };
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]