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/vernacentries.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/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index df39c617d3..df94f69cf6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -475,7 +475,7 @@ let program_inference_hook env sigma ev = Evarutil.is_ground_term sigma concl) then None else - let c, _, _, ctx = + let c, _, _, _, ctx = Declare.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac in Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c) |