diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 11:23:41 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 11:23:41 +0200 |
| commit | 77e4a3712dff87e5941dd93ebfa8028039ab0715 (patch) | |
| tree | ca9db76e334d40fb19938b014a20c3691866092a /stm/vernac_classifier.ml | |
| parent | 3e29266b1e2dfb970ca77fb5910b6a5860d4ad1a (diff) | |
| parent | 48476a32fa9221b216074695cceeaa0b34fc659b (diff) | |
Merge PR#717: [proof] Deprecate "proof mode" API
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index d597f64ad..471e05e45 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -10,7 +10,7 @@ open Vernacexpr open CErrors open Pp -let default_proof_mode () = Proof_global.get_default_proof_mode_name () +let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] let string_of_in_script b = if b then " (inside script)" else "" |