diff options
| author | Emilio Jesus Gallego Arias | 2019-05-22 05:33:10 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:54:43 +0200 |
| commit | fd2d2a8178d78e441fb3191cf112ed517dc791af (patch) | |
| tree | 8a85d441d2a25ad1ee4f46ef498694be9e9a8a12 /tactics | |
| parent | fb92bcc7830a084a4a204c4f58c44e83c180a9c9 (diff) | |
[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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |