From fd2d2a8178d78e441fb3191cf112ed517dc791af Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 May 2019 05:33:10 +0200 Subject: [proof] Remove duplicated universe polymorphic from decl_kinds This information is already present on `Proof.t`, so we extract it form there. Moreover, this information is essential to the lower-level proof, as opposed to the "kind" information which is only relevant to the vernac layer; we will move it thus to its proper layer in subsequent commits. --- tactics/abstract.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/abstract.ml b/tactics/abstract.ml index e4fa5e84b4..68a2a0afe0 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -103,8 +103,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = question, how does abstract behave when discharge is local for example? *) let goal_kind, suffix = if opaque - then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof" - else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in + then (Global ImportDefaultBehavior,Proof Theorem), "_subproof" + else (Global ImportDefaultBehavior,DefinitionBody Definition), "_subterm" in let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -141,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context evd in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~poly ~goal_kind id ectx 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 -- cgit v1.2.3