diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 03:40:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 17:38:19 +0100 |
| commit | dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 (patch) | |
| tree | 228d0aeba91a663b947625fd58cebe5bf4537f08 /dev | |
| parent | d7a5f439de0208c4a543a81158107b8ccecb6ced (diff) | |
[plugins] Prepare plugin API for functional handling of state.
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b4c8ae33c..5b09436c2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -508,7 +508,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context constr_display c) + (fun _ st -> in_current_context constr_display c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -524,7 +524,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context print_pure_constr c) + (fun _ st -> in_current_context print_pure_constr c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) |