aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/float_syntax.ml10
-rw-r--r--plugins/syntax/g_numeral.mlg4
-rw-r--r--plugins/syntax/g_string.mlg4
-rw-r--r--plugins/syntax/int63_syntax.ml4
-rw-r--r--plugins/syntax/numeral.ml4
-rw-r--r--plugins/syntax/numeral.mli4
-rw-r--r--plugins/syntax/r_syntax.ml6
-rw-r--r--plugins/syntax/r_syntax.mli4
-rw-r--r--plugins/syntax/string_notation.ml4
-rw-r--r--plugins/syntax/string_notation.mli4
10 files changed, 25 insertions, 23 deletions
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index 3c2e217d1c..23d4d63228 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_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 * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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) *)
(************************************************************************)
open Names
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 44c494e075..49d29e7b63 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
index c94119fdb0..788f9e011d 100644
--- a/plugins/syntax/g_string.mlg
+++ b/plugins/syntax/g_string.mlg
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index bfbf9d6b88..5f4db8e800 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 9808c61255..2250d57809 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 54e293c8b1..99252484b4 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index f6fbdaa958..7043653f7b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -134,7 +134,7 @@ let r_of_rawnum ?loc (sign,n) =
| '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2))
| '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2))))
| _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in
- Bigint.(sub e (of_int (String.length f))) in
+ Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' f))))) in
if Bigint.is_strictly_pos e then rmult n (izr (pow10 e))
else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e)))
else n (* e = 0 *)
diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli
index 87553dcb56..b72d544151 100644
--- a/plugins/syntax/r_syntax.mli
+++ b/plugins/syntax/r_syntax.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index c92acb0f55..e7ed0d8061 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index abdf4560d8..0d99f98d26 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * 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) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:15:48 +0000