aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml13
-rw-r--r--kernel/names.ml2
-rw-r--r--parsing/lexer.ml460
-rw-r--r--theories/Logic/ClassicalDescription.v2
-rw-r--r--theories/Logic/ClassicalFacts.v4
-rw-r--r--theories/Logic/ConstructiveEpsilon.v4
-rw-r--r--theories/Logic/Diaconescu.v2
-rw-r--r--theories/Numbers/Cyclic/Abstract/NZCyclic.v4
-rw-r--r--theories/Program/Utils.v6
-rw-r--r--theories/QArith/QArith_base.v2
-rw-r--r--toplevel/cerrors.ml15
11 files changed, 60 insertions, 54 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d2c2b0d6a8..6fc65e9fb7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -50,7 +50,7 @@ let for_grammar f x =
type internalisation_error =
| VariableCapture of identifier
| WrongExplicitImplicit
- | NegativeMetavariable
+ | IllegalMetavariable
| NotAConstructor of reference
| UnboundFixName of bool * identifier
| NonLinearPattern of identifier
@@ -66,8 +66,8 @@ let explain_wrong_explicit_implicit =
str "Found an explicitly given implicit argument but was expecting" ++
fnl () ++ str "a regular one"
-let explain_negative_metavariable =
- str "Metavariable numbers must be positive"
+let explain_illegal_metavariable =
+ str "Metavariables allowed only in patterns"
let explain_not_a_constructor ref =
str "Unknown constructor: " ++ pr_reference ref
@@ -102,7 +102,7 @@ let explain_bad_explicitation_number n po =
let explain_internalisation_error = function
| VariableCapture id -> explain_variable_capture id
| WrongExplicitImplicit -> explain_wrong_explicit_implicit
- | NegativeMetavariable -> explain_negative_metavariable
+ | IllegalMetavariable -> explain_illegal_metavariable
| NotAConstructor ref -> explain_not_a_constructor ref
| UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
| NonLinearPattern id -> explain_non_linear_pattern id
@@ -940,7 +940,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CPatVar (loc, n) when allow_patvar ->
RPatVar (loc, n)
| CPatVar (loc, _) ->
- raise (InternalisationError (loc,NegativeMetavariable))
+ raise (InternalisationError (loc,IllegalMetavariable))
| CEvar (loc, n, l) ->
REvar (loc, n, Option.map (List.map (intern env)) l)
| CSort (loc, s) ->
@@ -1093,7 +1093,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
intern env c
with
InternalisationError (loc,e) ->
- user_err_loc (loc,"internalize",explain_internalisation_error e)
+ user_err_loc (loc,"internalize",
+ explain_internalisation_error e ++ str ".")
(**************************************************************************)
(* Functions to translate constr_expr into rawconstr *)
diff --git a/kernel/names.ml b/kernel/names.ml
index 3d80ad23e8..0191880d16 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -103,7 +103,7 @@ let label_of_mbid (_,s,_) = s
let mk_label l = l
-let string_of_label l = l
+let string_of_label = string_of_id
let id_of_label l = l
let label_of_id id = id
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index b04ab971e4..d7fa2b5753 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -324,43 +324,49 @@ let rec comment bp = parser bp2
(* Parse a special token, using the [token_tree] *)
(* Peek as much utf-8 lexemes as possible *)
-(* then look if a special token is obtained *)
-let rec special tt cs =
- match Stream.peek cs with
- | Some c -> progress_from_byte 0 tt cs c
- | None -> tt.node
-
- (* nr is the number of char peeked; n the number of char in utf8 block *)
-and progress_utf8 nr n c tt cs =
+(* and retain the longest valid special token obtained *)
+let rec progress_further last nj tt cs =
+ try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
+ with Failure _ -> last
+
+and update_longest_valid_token last nj tt cs =
+ match tt.node with
+ | Some _ as last' ->
+ for i=1 to nj do Stream.junk cs done;
+ progress_further last' 0 tt cs
+ | None ->
+ progress_further last nj tt cs
+
+(* nr is the number of char peeked since last valid token *)
+(* n the number of char in utf8 block *)
+and progress_utf8 last nj n c tt cs =
try
let tt = CharMap.find c tt.branch in
- let tt =
- if n=1 then tt else
- match Stream.npeek (n-nr) cs with
- | l when List.length l = n-nr ->
- let l = Util.list_skipn (1-nr) l in
- List.iter (check_utf8_trailing_byte cs) l;
- List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l
- | _ ->
- error_utf8 cs
- in
- for i=1 to n-nr do Stream.junk cs done;
- special tt cs
+ if n=1 then
+ update_longest_valid_token last (nj+n) tt cs
+ else
+ match Util.list_skipn (nj+1) (Stream.npeek (nj+n) cs) with
+ | l when List.length l = n-1 ->
+ List.iter (check_utf8_trailing_byte cs) l;
+ let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in
+ update_longest_valid_token last (nj+n) tt cs
+ | _ ->
+ error_utf8 cs
with Not_found ->
- tt.node
+ last
-and progress_from_byte nr tt cs = function
+and progress_from_byte last nj tt cs = function
(* Utf8 leading byte *)
- | '\x00'..'\x7F' as c -> progress_utf8 nr 1 c tt cs
- | '\xC0'..'\xDF' as c -> progress_utf8 nr 2 c tt cs
- | '\xE0'..'\xEF' as c -> progress_utf8 nr 3 c tt cs
- | '\xF0'..'\xF7' as c -> progress_utf8 nr 4 c tt cs
+ | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs
+ | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs
+ | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs
+ | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs
| _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) ->
error_utf8 cs
(* Must be a special token *)
let process_chars bp c cs =
- let t = progress_from_byte 1 !token_tree cs c in
+ let t = progress_from_byte None (-1) !token_tree cs c in
let ep = Stream.count cs in
match t with
| Some t -> (("", t), (bp, ep))
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index aa65eb44c8..8555886023 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -21,7 +21,7 @@ Set Implicit Arguments.
Require Export Classical.
Require Import ChoiceFacts.
-Notation Local "'inhabited' A" := A (at level 200, only parsing).
+Notation Local inhabited A := A.
Axiom constructive_definite_description :
forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index f3f177a734..6673fa8c96 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -119,7 +119,7 @@ Qed.
*)
-Definition inhabited (A:Prop) := A.
+Notation Local inhabited A := A.
Lemma prop_ext_A_eq_A_imp_A :
prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
@@ -514,8 +514,6 @@ Qed.
344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
*)
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
-
Definition IndependenceOfGeneralPremises :=
forall (A:Type) (P:A -> Prop) (Q:Prop),
inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index fe571779ca..83d5e002aa 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id:$ i*)
+(*i $Id$ i*)
(** This module proves the constructive description schema, which
infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -53,7 +53,7 @@ of our searching algorithm. *)
Let R (x y : nat) : Prop := x = S y /\ ~ P y.
-Notation Local "'acc' x" := (Acc R x) (at level 10).
+Notation Local acc x := (Acc R x).
Lemma P_implies_acc : forall x : nat, P x -> acc x.
Proof.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index a954cbef7d..b96ae30e4e 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM.
(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
+Notation Local inhabited A := A.
Section ExtensionalEpsilon_imp_EM.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 92ada3d748..125fd3f127 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -89,8 +89,8 @@ Open Local Scope IntScope.
Notation "x == y" := (NZeq x y) (at level 70) : IntScope.
Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
Notation "0" := NZ0 : IntScope.
-Notation "'S'" := NZsucc : IntScope.
-Notation "'P'" := NZpred : IntScope.
+Notation S x := (NZsucc x).
+Notation P x := (NZpred x).
(*Notation "1" := (S 0) : IntScope.*)
Notation "x + y" := (NZadd x y) : IntScope.
Notation "x - y" := (NZsub x y) : IntScope.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index c4a20506c7..149901c7bb 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -42,8 +42,8 @@ Notation dec := sumbool_of_bool.
(** Hide proofs and generates obligations when put in a term. *)
-Notation "'in_left'" := (@left _ _ _) : program_scope.
-Notation "'in_right'" := (@right _ _ _) : program_scope.
+Notation in_left := (@left _ _ _).
+Notation in_right := (@right _ _ _).
(** Extraction directives *)
(*
@@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
(* Extract Inductive sigT => "prod" [ "" ]. *)
-*) \ No newline at end of file
+*)
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 9ebfa19cb4..f4b57d5bed 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -31,7 +31,7 @@ Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
Definition inject_Z (x : Z) := Qmake x 1.
Arguments Scope inject_Z [Z_scope].
-Notation " 'QDen' p " := (Zpos (Qden p)) (at level 20, no associativity) : Q_scope.
+Notation QDen p := (Zpos (Qden p)).
Notation " 0 " := (0#1) : Q_scope.
Notation " 1 " := (1#1) : Q_scope.
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index bad30a8491..b11592ba48 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -34,17 +34,17 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
| Stream.Failure ->
hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
| Stream.Error txt ->
- hov 0 (str "Syntax error: " ++ str txt)
+ hov 0 (str "Syntax error: " ++ str txt ++ str ".")
| Token.Error txt ->
- hov 0 (str "Syntax error: " ++ str txt)
+ hov 0 (str "Syntax error: " ++ str txt ++ str ".")
| Sys_error msg ->
hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
| UserError(s,pps) ->
hov 1 (str "User error: " ++ where s ++ pps)
| Out_of_memory ->
- hov 0 (str "Out of memory")
+ hov 0 (str "Out of memory.")
| Stack_overflow ->
- hov 0 (str "Stack overflow")
+ hov 0 (str "Stack overflow.")
| Anomaly (s,pps) ->
hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ())
| Match_failure(filename,pos1,pos2) ->
@@ -94,10 +94,11 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (str "Error:" ++ spc () ++
str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
spc () ++ str "was not found" ++
- spc () ++ str "in the current" ++ spc () ++ str "environment")
+ spc () ++ str "in the current" ++ spc () ++ str "environment.")
| Nametab.GlobalizationConstantError q ->
hov 0 (str "Error:" ++ spc () ++
- str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
+ str "No constant of this name:" ++ spc () ++
+ Libnames.pr_qualid q ++ str ".")
| Refiner.FailError (i,s) ->
hov 0 (str "Error: Tactic failure" ++ s ++
if i=0 then mt () else str " (level " ++ int i ++ str").")
@@ -145,7 +146,7 @@ let raise_if_debug e =
let _ = Tactic_debug.explain_logic_error := explain_exn_default
let _ = Tactic_debug.explain_logic_error_no_anomaly :=
- explain_exn_default_aux (fun () -> mt()) (fun () -> mt())
+ explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
let explain_exn_function = ref explain_exn_default
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-22 13:27:28 +0000