Dm.UtilitiesSourceval shift_feedback :
start:int ->
offset:int ->
('a * Loc.t option * 'b * 'c) ->
'a * Loc.t option * 'b * 'cval shift_checking_result :
start:int ->
offset:int ->
Types.sentence_checking_result ->
Types.sentence_checking_resultReturns the vernac state after the sentence
val get_proof_context :
Types.sentence_checking_result option ->
(Evd.evar_map * Environ.env) option