diff options
| author | Maxime Dénès | 2018-04-12 20:20:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-12 20:20:15 +0200 |
| commit | 424cffe91ee8819de8cde27d98c534eed51ca251 (patch) | |
| tree | 7cb695d8478f69694e1d7a51ff16c679204f819a /stm | |
| parent | de828ea7d9991d4509156ce2ae073011998e65b5 (diff) | |
| parent | 2dbb54b1bc3967ee5d6e838cce8c56b88bd9477d (diff) | |
Merge PR #7194: [warnings] Remove `set_current_loc` hack.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index ba0a2017a3..30aa9ea06e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -3013,7 +3013,6 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++ str "This is not supported yet, sorry."); let indentation, strlen = compute_indentation ?loc ontop in - CWarnings.set_current_loc loc; (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = Vernac_classifier.classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in @@ -3037,7 +3036,6 @@ let query ~doc ~at ~route s = while true do let { CAst.loc; v=ast } = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in - CWarnings.set_current_loc loc; let st = State.get_cached at in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in ignore(stm_vernac_interp ~route at st aast) |