diff options
| author | Emilio Jesus Gallego Arias | 2020-04-10 03:46:57 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-03 17:25:55 +0200 |
| commit | eab9f3bd104f154c128955ff344eb671d0e2ec93 (patch) | |
| tree | bea8faeeb4f6f71cd80143d72dd61ea628b06579 /vernac/pfedit.ml | |
| parent | d4081616fafe3e9fa02cef2e0102a03638f70fd6 (diff) | |
[funind] Remove use of low-level entries in scheme generation.
This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.
Some more cleanup needs to be done but this is clearly a step forward
IMHO.
Diffstat (limited to 'vernac/pfedit.ml')
| -rw-r--r-- | vernac/pfedit.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml index d6b9592176..1b34b6ec28 100644 --- a/vernac/pfedit.ml +++ b/vernac/pfedit.ml @@ -5,5 +5,9 @@ let by = Declare.by let refine_by_tactic = Proof.refine_by_tactic (* We don't want to export this anymore, but we do for now *) -let build_by_tactic = Declare.build_by_tactic +let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac = + let b, t, _unis, safe, uctx = + Declare.build_by_tactic ?side_eff env ~uctx ~poly ~typ tac in + b, t, safe, uctx + let build_constant_by_tactic = Declare.build_constant_by_tactic |