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/declare.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/declare.ml')
| -rw-r--r-- | vernac/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 357f58feea..95e573a671 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -762,7 +762,7 @@ let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ t 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 = Environ.(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, uctx = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in let cb, uctx = if side_eff then inline_private_constants ~uctx env ce else @@ -770,7 +770,7 @@ let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac = let (cb, ctx), _eff = Future.force ce.proof_entry_body in cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx in - cb, ce.proof_entry_type, status, univs + cb, ce.proof_entry_type, ce.proof_entry_universes, status, uctx let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl = (* EJGA: flush_and_check_evars is only used in abstract, could we |