diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 01:50:26 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:10 -0400 |
| commit | 92b61209c60b368bbc095950786187b94b167632 (patch) | |
| tree | 5cceb7b23780618d89143d674aca2b3ccb481742 /tactics | |
| parent | 139d206294f98194e9bdb19a7d5da73f9b104db5 (diff) | |
[declare] Remove one use of inline_private_constants
We instead favor the `build_by_tactic` function which should at some
point better integrated in the declare core.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pfedit.ml | 6 | ||||
| -rw-r--r-- | tactics/pfedit.mli | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 438892e75e..a2edb5fe49 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -129,10 +129,10 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~ | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") -let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = +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 sigma sign ~poly typ tac in + let ce, status, univs = build_constant_by_tactic ~name uctx sign ~poly typ tac in let cb, univs = if side_eff then Declare.inline_private_constants ~univs env ce else @@ -140,7 +140,7 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx in - cb, status, univs + cb, ce.Declare.proof_entry_type, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = (* Save the initial side-effects to restore them afterwards. We set the diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 3cf3a13262..c1f656376d 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -74,11 +74,11 @@ val build_constant_by_tactic val build_by_tactic : ?side_eff:bool -> env - -> UState.t + -> uctx:UState.t -> poly:bool - -> EConstr.types + -> typ:EConstr.types -> unit Proofview.tactic - -> constr * bool * UState.t + -> constr * types option * bool * UState.t val refine_by_tactic : name:Id.t |