diff options
| author | Emilio Jesus Gallego Arias | 2020-04-04 05:20:46 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-19 14:32:21 +0200 |
| commit | 0643873397552cc2fe4d1486c14f206968dea672 (patch) | |
| tree | 3514ec170fcdd74916c491ae9e99ba16630097c8 | |
| parent | d97499e1dc8644821a0b9d70bf4dcd479bd1df26 (diff) | |
[declare] Remove unused parameters in prepare_obligation
| -rw-r--r-- | vernac/comDefinition.ml | 2 | ||||
| -rw-r--r-- | vernac/declare.ml | 2 | ||||
| -rw-r--r-- | vernac/declare.mli | 6 |
3 files changed, 3 insertions, 7 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index eac8f92e2e..d56917271c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in + let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls diff --git a/vernac/declare.ml b/vernac/declare.ml index 0b03a63d09..3ffde76790 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1007,7 +1007,7 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry -let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = +let prepare_obligation ~name ~types ~body sigma = let env = Global.env () in let types = match types with | Some t -> t diff --git a/vernac/declare.mli b/vernac/declare.mli index 82b0cff8d9..62bc6a34bf 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -367,11 +367,7 @@ val declare_mutually_recursive (** Prepare API, to be removed once we provide the corresponding 1-step API *) val prepare_obligation - : ?opaque:bool - -> ?inline:bool - -> name:Id.t - -> poly:bool - -> udecl:UState.universe_decl + : name:Id.t -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map |