diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 07:00:09 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:55 -0400 |
| commit | 1a18c20ba374a74bc7dda0c4719258b93afb149e (patch) | |
| tree | b024009ebac5046b3ecb2e52470ea8d69ff4a0ab | |
| parent | b5f5e9d0de635193ee9ee8569809c25d369b1fcc (diff) | |
[pfedit] Labelize sign parameter
| -rw-r--r-- | tactics/abstract.ml | 2 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 4 | ||||
| -rw-r--r-- | tactics/pfedit.mli | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 9aa5170a29..e85d94cd72 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -91,7 +91,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 sigma in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~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 diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index c02b198bf7..b228a04298 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -116,7 +116,7 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx sign ~poly typ tac = +let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sign ~poly typ tac = let evd = Evd.from_ctx uctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in @@ -132,7 +132,7 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx sign let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let ce, status, univs = build_constant_by_tactic ~name ~uctx sign ~poly typ tac in + let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in let cb, uctx = if side_eff then Declare.inline_private_constants ~uctx env ce else diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 8085153df0..c49e997757 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -65,7 +65,7 @@ val build_constant_by_tactic : name:Id.t -> ?opaque:Proof_global.opacity_flag -> uctx:UState.t - -> named_context_val + -> sign:named_context_val -> poly:bool -> EConstr.types -> unit Proofview.tactic |