aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/g_numeral.mlg21
-rw-r--r--plugins/syntax/g_string.mlg21
-rw-r--r--plugins/syntax/int63_syntax.ml10
-rw-r--r--plugins/syntax/numeral.ml6
-rw-r--r--plugins/syntax/numeral.mli4
-rw-r--r--plugins/syntax/r_syntax.ml2
-rw-r--r--plugins/syntax/r_syntax.mli2
-rw-r--r--plugins/syntax/string_notation.ml6
-rw-r--r--plugins/syntax/string_notation.mli4
9 files changed, 26 insertions, 50 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 0f0f3953da..44c494e075 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -34,23 +34,8 @@ VERNAC ARGUMENT EXTEND numnotoption
END
VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
- | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+ | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
ident(sc) numnotoption(o) ] ->
- { (* It is a bug to use the proof context here, but at the request of
- * the reviewers we keep this broken behavior for now. The Global env
- * should be used instead, and the `env, sigma` parameteter to the
- * numeral notation command removed.
- *)
- fun ~pstate ->
- let sigma, env = match pstate with
- | None ->
- let env = Global.env () in
- let sigma = Evd.from_env env in
- sigma, env
- | Some pstate ->
- Pfedit.get_current_context pstate
- in
- vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o;
- pstate }
+ { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
END
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
index cc8c13a84b..c94119fdb0 100644
--- a/plugins/syntax/g_string.mlg
+++ b/plugins/syntax/g_string.mlg
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -19,22 +19,7 @@ open Stdarg
}
VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
- | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+ | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
ident(sc) ] ->
- { (* It is a bug to use the proof context here, but at the request of
- * the reviewers we keep this broken behavior for now. The Global env
- * should be used instead, and the `env, sigma` parameteter to the
- * numeral notation command removed.
- *)
- fun ~pstate ->
- let sigma, env = match pstate with
- | None ->
- let env = Global.env () in
- let sigma = Evd.from_env env in
- sigma, env
- | Some pstate ->
- Pfedit.get_current_context pstate
- in
- vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc);
- pstate }
+ { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
END
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index 992b7a986b..bfbf9d6b88 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index ec8c2338fb..0a1cc8745d 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -101,7 +101,9 @@ let type_error_of g ty =
str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
-let vernac_numeral_notation env sigma local ty f g scope opts =
+let vernac_numeral_notation local ty f g scope opts =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let dec_ty = locate_decimal () in
let z_pos_ty = locate_z () in
let int63_ty = locate_int63 () in
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index b14ed18497..54e293c8b1 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -14,6 +14,6 @@ open Notation
(** * Numeral notation *)
-val vernac_numeral_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+val vernac_numeral_notation : locality_flag ->
qualid -> qualid -> qualid ->
Notation_term.scope_name -> numnot_option -> unit
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index b9062dd16b..1cbc86b6fe 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli
index 7c3ee60040..87553dcb56 100644
--- a/plugins/syntax/r_syntax.mli
+++ b/plugins/syntax/r_syntax.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 5fae696d58..bc586acce7 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -47,7 +47,9 @@ let type_error_of g ty =
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
-let vernac_string_notation env sigma local ty f g scope =
+let vernac_string_notation local ty f g scope =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let app x y = mkAppC (x,[y]) in
let cref q = mkRefC q in
let cbyte = cref (q_byte ()) in
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index e81de603d9..abdf4560d8 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -13,6 +13,6 @@ open Vernacexpr
(** * String notation *)
-val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+val vernac_string_notation : locality_flag ->
qualid -> qualid -> qualid ->
Notation_term.scope_name -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 11:04:34 +0000