[declare] [abstract] Do evars check in declare_abstract

This makes sense as it is mandatory for the client.

3 files changed, 15 insertions, 14 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 194dfacf60..0e78a03f45 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -11,7 +11,6 @@
 open Util
 open Termops
 open EConstr
-open Evarutil
 
 module NamedDecl = Context.Named.Declaration
 
@@ -76,10 +75,6 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
               | None ->  Proofview.Goal.concl gl
               | Some ty -> ty in
   let concl = it_mkNamedProd_or_LetIn concl sign in
-  let concl =
-    try flush_and_check_evars sigma concl
-    with Uninstantiated_evar _ ->
-      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let effs, sigma, lem, args, safe =
     Declare.declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index adcf3e247d..e1ddf262a0 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -807,16 +807,22 @@ let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
   cb, ce.proof_entry_type, status, univs
 
 let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
-  let sigma, ctx, concl =
+  (* EJGA: flush_and_check_evars is only used in abstract, could we
+     use a different API? *)
+  let concl =
+    try Evarutil.flush_and_check_evars sigma concl
+    with Evarutil.Uninstantiated_evar _ ->
+      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
+  in
+  let sigma, concl =
     (* FIXME: should be done only if the tactic succeeds *)
     let sigma = Evd.minimize_universes sigma in
-    let ctx = Evd.universe_context_set sigma in
-    sigma, ctx, Evarutil.nf_evars_universes sigma concl
+    sigma, Evarutil.nf_evars_universes sigma concl
   in
   let concl = EConstr.of_constr concl in
-  let ectx = Evd.evar_universe_context sigma in
-  let (const, safe, ectx) =
-    try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac
+  let uctx = Evd.evar_universe_context sigma in
+  let (const, safe, uctx) =
+    try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~sign:secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
@@ -825,6 +831,7 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c
     let (_, info) = Exninfo.capture src in
     Exninfo.iraise (e, info)
   in
+  let sigma = Evd.set_universe_context sigma uctx in
   let body, effs = Future.force const.proof_entry_body in
   (* We drop the side-effects from the entry, they already exist in the ambient environment *)
   let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in
@@ -854,7 +861,6 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c
   in
   let args = List.map EConstr.of_constr args in
   let lem = EConstr.mkConstU (cst, inst) in
-  let sigma = Evd.set_universe_context sigma ectx in
   let effs = Evd.concat_side_effects eff effs in
   effs, sigma, lem, args, safe
 
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 58786f724d..ff8a705e60 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -257,7 +257,7 @@ val get_open_goals : t -> int
     Returns [false] if an unsafe tactic has been used. *)
 val by : unit Proofview.tactic -> t -> t * bool
 
-(** Declare abstract constant *)
+(** Declare abstract constant; will check no evars are possible; *)
 val declare_abstract :
      name:Names.Id.t
   -> poly:bool
@@ -267,7 +267,7 @@ val declare_abstract :
   -> opaque:bool
   -> solve_tac:unit Proofview.tactic
   -> Evd.evar_map
-  -> Constr.t
+  -> EConstr.t
   -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool
 
 val build_by_tactic