diff options
| author | Gaëtan Gilbert | 2018-10-11 18:21:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | 9a1e658860b6320830698f197b69694c661ecfa0 (patch) | |
| tree | 069c9bd39fcf0cbd33f1f1f1849b859d3d4b1296 | |
| parent | 1b753da49ea4a10d7779bb50d93bea25157c01bd (diff) | |
Add comment in stm to unsupport attributes for special commands
| -rw-r--r-- | stm/stm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 19915b1600..07049815ef 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1077,6 +1077,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | _ -> false in let aux_interp st expr = + (* XXX unsupported attributes *) let cmd = Vernacprop.under_control expr in if is_filtered_command cmd then (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) |