diff options
| -rw-r--r-- | tactics/abstract.ml | 5 | ||||
| -rw-r--r-- | tactics/declare.ml | 20 | ||||
| -rw-r--r-- | tactics/declare.mli | 4 |
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 |