aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--configure.ml21
-rw-r--r--dev/printers.mllib2
-rw-r--r--grammar/argextend.ml42
-rw-r--r--ide/coqOps.ml24
-rw-r--r--lib/pp.mli2
-rw-r--r--library/declaremods.ml6
-rw-r--r--ltac/tacentries.ml8
-rw-r--r--ltac/tacinterp.ml2
-rw-r--r--parsing/cLexer.ml4 (renamed from parsing/lexer.ml4)0
-rw-r--r--parsing/cLexer.mli (renamed from parsing/lexer.mli)0
-rw-r--r--parsing/compat.ml42
-rw-r--r--parsing/egramcoq.ml6
-rw-r--r--parsing/egramml.ml2
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_prim.ml42
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/parsing.mllib2
-rw-r--r--parsing/pcoq.ml4
-rw-r--r--test-suite/bugs/closed/4713.v10
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v84
-rw-r--r--toplevel/cerrors.ml2
-rw-r--r--toplevel/coqloop.ml2
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/metasyntax.ml14
-rw-r--r--toplevel/obligations.ml14
-rw-r--r--toplevel/vernac.ml8
28 files changed, 162 insertions, 69 deletions
diff --git a/.gitignore b/.gitignore
index b50bca3cf..4127ac649 100644
--- a/.gitignore
+++ b/.gitignore
@@ -125,7 +125,7 @@ grammar/q_constr.ml
grammar/tacextend.ml
grammar/vernacextend.ml
grammar/argextend.ml
-parsing/lexer.ml
+parsing/cLexer.ml
tactics/hipattern.ml
ltac/coretactics.ml
ltac/extratactics.ml
diff --git a/configure.ml b/configure.ml
index 5baaf6d8c..6adaa45db 100644
--- a/configure.ml
+++ b/configure.ml
@@ -251,7 +251,6 @@ module Prefs = struct
let debug = ref false
let profile = ref false
let annotate = ref false
- let makecmd = ref "make"
let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
let coqwebsite = ref "http://coq.inria.fr/"
let force_caml_version = ref false
@@ -329,14 +328,14 @@ let args_options = Arg.align [
" Add profiling information in the Coq executables";
"-annotate", Arg.Set Prefs.annotate,
" Dumps ml annotation files while compiling Coq";
- "-makecmd", Arg.Set_string Prefs.makecmd,
- "<command> Name of GNU Make command";
+ "-makecmd", Arg.String (fun _ -> printf "Warning: obsolete -makecmd option\n"),
+ "<command> Obsolete: name of GNU Make command";
"-native-compiler", arg_bool Prefs.nativecompiler,
"(yes|no) Compilation to native code for conversion and normalization";
"-coqwebsite", Arg.Set_string Prefs.coqwebsite,
" URL of the coq website";
"-force-caml-version", Arg.Set Prefs.force_caml_version,
- "Force OCaml version";
+ " Force OCaml version";
]
let parse_args () =
@@ -423,18 +422,6 @@ let vcs =
else if dir_exists "{arch}" then "gnuarch"
else "none"
-(** * The make command *)
-
-let make =
- try
- let version_line, _ = run !Prefs.makecmd ["-v"] in
- let version = List.nth (string_split ' ' version_line) 2 in
- match string_split '.' version with
- | major::minor::_ when (s2i major, s2i minor) >= (3,81) ->
- printf "You have GNU Make %s. Good!\n" version
- | _ -> failwith "bad version"
- with _ -> die "Error: Cannot find GNU Make >= 3.81."
-
(** * Browser command *)
let browser =
@@ -834,7 +821,7 @@ let strip =
(** * md5sum command *)
let md5sum =
- if arch = "Darwin" then "md5 -q" else "md5sum"
+ if arch = "Darwin" || arch = "FreeBSD" then "md5 -q" else "md5sum"
(** * Documentation : do we have latex, hevea, ... *)
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 5d10f54fb..390a9f384 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -161,7 +161,7 @@ Library
States
Genprint
-Lexer
+CLexer
Ppextend
Pputils
Ppannotation
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 3b7e180c6..0e52dc948 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -40,7 +40,7 @@ let make_act loc act pil =
make (List.rev pil)
let make_prod_item = function
- | ExtTerminal s -> <:expr< Extend.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
+ | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >>
| ExtNonTerminal (g, _) ->
let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
mlexpr_of_prod_entry_key base g
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6639b0201..b55786ddd 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -12,7 +12,9 @@ open Ideutils
open Interface
open Feedback
-type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string ]
+let b2c = byte_offset_to_char_offset
+
+type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string ]
type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ]
let mem_flag_of_flag : flag -> mem_flag = function
| `ERROR _ -> `ERROR
@@ -396,8 +398,8 @@ object(self)
let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
let pre_chars, post_chars =
if Loc.is_ghost loc then 0, String.length phrase else Loc.unloc loc in
- let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in
- let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in
+ let pre = b2c phrase pre_chars in
+ let post = b2c phrase post_chars in
let start = start_sentence#forward_chars pre in
let stop = start_sentence#forward_chars post in
let markup = Glib.Markup.escape_text text in
@@ -461,7 +463,7 @@ object(self)
| ErrorMsg(loc, msg), Some (id,sentence) ->
log "ErrorMsg" id;
remove_flag sentence `PROCESSING;
- add_flag sentence (`ERROR msg);
+ add_flag sentence (`ERROR (loc, msg));
self#mark_as_needed sentence;
self#attach_tooltip sentence loc msg;
if not (Loc.is_ghost loc) then
@@ -500,8 +502,8 @@ object(self)
| None -> ()
| Some (start, stop) ->
buffer#apply_tag Tags.Script.error
- ~start:(iter#forward_chars (byte_offset_to_char_offset phrase start))
- ~stop:(iter#forward_chars (byte_offset_to_char_offset phrase stop))
+ ~start:(iter#forward_chars (b2c phrase start))
+ ~stop:(iter#forward_chars (b2c phrase stop))
method private position_error_tag_at_sentence sentence loc =
let start, _, phrase = self#get_sentence sentence in
@@ -652,7 +654,15 @@ object(self)
method get_errors =
let extract_error s =
match List.find (function `ERROR _ -> true | _ -> false) s.flags with
- | `ERROR msg -> (buffer#get_iter_at_mark s.start)#line + 1, msg
+ | `ERROR (loc, msg) ->
+ let iter =
+ if Loc.is_ghost loc then
+ buffer#get_iter_at_mark s.start
+ else
+ let (iter, _, phrase) = self#get_sentence s in
+ let (start, _) = Loc.unloc loc in
+ iter#forward_chars (b2c phrase start) in
+ iter#line + 1, msg
| _ -> assert false in
List.rev
(Doc.fold_all document [] (fun acc _ _ s ->
diff --git a/lib/pp.mli b/lib/pp.mli
index 2e4d02974..04a60a7c8 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -168,7 +168,7 @@ val is_message : Xml_datatype.xml -> bool
*
* Morally the parser gets a string and an edit_id, and gives back an AST.
* Feedbacks during the parsing phase are attached to this edit_id.
- * The interpreter assignes an exec_id to the ast, and feedbacks happening
+ * The interpreter assigns an exec_id to the ast, and feedbacks happening
* during interpretation are attached to the exec_id.
* Only one among state_id and edit_id can be provided. *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 701c15e14..f3f734aa0 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -642,7 +642,11 @@ let declare_module interp_modast id args res mexpr_o fs =
let env = Global.env () in
let mty_entry_o, subs, inl_res = match res with
| Enforce (mty,ann) ->
- Some (fst (interp_modast env ModType mty)), [], inl2intopt ann
+ let inl = inl2intopt ann in
+ let mte, _ = interp_modast env ModType mty in
+ (* We check immediately that mte is well-formed *)
+ let _ = Mod_typing.translate_mse env None inl mte in
+ Some mte, [], inl
| Check mtys ->
None, build_subtypes interp_modast env mp arg_entries_r mtys,
default_inline ()
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index f1b8eee5e..881482081 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -397,11 +397,11 @@ let create_ltac_quotation name cast (e, l) =
let assoc = None in
let rule =
Next (Next (Next (Next (Next (Stop,
- Atoken (Lexer.terminal name)),
- Atoken (Lexer.terminal ":")),
- Atoken (Lexer.terminal "(")),
+ Atoken (CLexer.terminal name)),
+ Atoken (CLexer.terminal ":")),
+ Atoken (CLexer.terminal "(")),
entry),
- Atoken (Lexer.terminal ")"))
+ Atoken (CLexer.terminal ")"))
in
let action _ v _ _ _ loc = cast (loc, v) in
let gram = (level, assoc, [Rule (rule, action)]) in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 6a5d1380d..d650cb5c6 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -552,7 +552,7 @@ let interp_fresh_id ist env sigma l =
String.concat "" (List.map (function
| ArgArg s -> s
| ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in
- let s = if Lexer.is_keyword s then s^"0" else s in
+ let s = if CLexer.is_keyword s then s^"0" else s in
Id.of_string s in
Tactics.fresh_id_in_env avoid id env
diff --git a/parsing/lexer.ml4 b/parsing/cLexer.ml4
index 8b8b38c34..8b8b38c34 100644
--- a/parsing/lexer.ml4
+++ b/parsing/cLexer.ml4
diff --git a/parsing/lexer.mli b/parsing/cLexer.mli
index 24b0ec847..24b0ec847 100644
--- a/parsing/lexer.mli
+++ b/parsing/cLexer.mli
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 1747aa535..310a44149 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -135,7 +135,7 @@ let to_coq_position = function
END
-(** Signature of Lexer *)
+(** Signature of CLexer *)
IFDEF CAMLP5 THEN
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 04b622864..eff666c9c 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -265,9 +265,9 @@ let recover_constr_grammar ntn prec =
(* Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
-type frozen_t = (int * GrammarCommand.t) list * Lexer.frozen_t
+type frozen_t = (int * GrammarCommand.t) list * CLexer.frozen_t
-let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
+let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ())
(* We compare the current state of the grammar and the state to unfreeze,
by computing the longest common suffixes *)
@@ -283,7 +283,7 @@ let unfreeze (grams, lex) =
remove_grammars n;
remove_levels n;
grammar_state := common;
- Lexer.unfreeze lex;
+ CLexer.unfreeze lex;
List.iter extend_dyn_grammar (List.rev_map snd redo)
(** No need to provide an init function : the grammar state is
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 95ac87247..97a3e89a5 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -33,7 +33,7 @@ let rec ty_rule_of_gram = function
| [] -> AnyTyRule TyStop
| GramTerminal s :: rem ->
let AnyTyRule rem = ty_rule_of_gram rem in
- let tok = Atoken (Lexer.terminal s) in
+ let tok = Atoken (CLexer.terminal s) in
let r = TyNext (rem, tok, None) in
AnyTyRule r
| GramNonTerminal (_, t, tok) :: rem ->
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7e470e844..243f71416 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -29,7 +29,7 @@ let constr_kw =
"Prop"; "Set"; "Type"; ".("; "_"; "..";
"`{"; "`("; "{|"; "|}" ]
-let _ = List.iter Lexer.add_keyword constr_kw
+let _ = List.iter CLexer.add_keyword constr_kw
let mk_cast = function
(c,(_,None)) -> c
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 5e67e9957..0d72f7b93 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -15,7 +15,7 @@ open Pcoq
open Pcoq.Prim
let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
-let _ = List.iter Lexer.add_keyword prim_kw
+let _ = List.iter CLexer.add_keyword prim_kw
let local_make_qualid l id = make_qualid (DirPath.make l) id
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 0c90a8bca..1a27d9692 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -25,7 +25,7 @@ open Pcoq
let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta]
let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter Lexer.add_keyword tactic_kw
+let _ = List.iter CLexer.add_keyword tactic_kw
let err () = raise Stream.Failure
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 35ba9757d..df42d9084 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -26,7 +26,7 @@ open Pcoq.Vernac_
open Pcoq.Module
let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
-let _ = List.iter Lexer.add_keyword vernac_kw
+let _ = List.iter CLexer.add_keyword vernac_kw
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 024d8607f..b052b6ee6 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,6 @@
Tok
Compat
-Lexer
+CLexer
Entry
Pcoq
Egramml
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fe9ab630f..6dcf76da8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -15,14 +15,14 @@ open Genarg
(** The parser of Coq *)
-module G = GrammarMake (Lexer)
+module G = GrammarMake (CLexer)
let warning_verbose = Compat.warning_verbose
module Symbols = GramextMake(G)
let gram_token_of_token = Symbols.stoken
-let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
+let gram_token_of_string s = gram_token_of_token (CLexer.terminal s)
let camlp4_verbosity silent f x =
let a = !warning_verbose in
diff --git a/test-suite/bugs/closed/4713.v b/test-suite/bugs/closed/4713.v
new file mode 100644
index 000000000..5d4d73be3
--- /dev/null
+++ b/test-suite/bugs/closed/4713.v
@@ -0,0 +1,10 @@
+Module Type T.
+ Parameter t : Type.
+End T.
+Module M : T.
+ Definition t := unit.
+End M.
+
+Fail Module Z : T with Module t := M := M.
+Fail Module Z <: T with Module t := M := M.
+Fail Declare Module Z : T with Module t := M.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 58b1b0180..d0168bd9e 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -8,8 +8,88 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-Require Import PeanoNat NAxioms.
+Require Import PeanoNat Even NAxioms.
-(** * [PeanoNat.Nat] already implements [NAxiomSig] *)
+(** This file is DEPRECATED ! Use [PeanoNat] (or [Arith]) instead. *)
+
+(** [PeanoNat.Nat] already implements [NAxiomSig] *)
Module Nat <: NAxiomsSig := Nat.
+
+(** Compat notations for stuff that used to be at the beginning of NPeano. *)
+
+Notation leb := Nat.leb (compat "8.4").
+Notation ltb := Nat.ltb (compat "8.4").
+Notation leb_le := Nat.leb_le (compat "8.4").
+Notation ltb_lt := Nat.ltb_lt (compat "8.4").
+Notation pow := Nat.pow (compat "8.4").
+Notation pow_0_r := Nat.pow_0_r (compat "8.4").
+Notation pow_succ_r := Nat.pow_succ_r (compat "8.4").
+Notation square := Nat.square (compat "8.4").
+Notation square_spec := Nat.square_spec (compat "8.4").
+Notation Even := Nat.Even (compat "8.4").
+Notation Odd := Nat.Odd (compat "8.4").
+Notation even := Nat.even (compat "8.4").
+Notation odd := Nat.odd (compat "8.4").
+Notation even_spec := Nat.even_spec (compat "8.4").
+Notation odd_spec := Nat.odd_spec (compat "8.4").
+
+Lemma Even_equiv n : Even n <-> Even.even n.
+Proof. symmetry. apply Even.even_equiv. Qed.
+Lemma Odd_equiv n : Odd n <-> Even.odd n.
+Proof. symmetry. apply Even.odd_equiv. Qed.
+
+Notation divmod := Nat.divmod (compat "8.4").
+Notation div := Nat.div (compat "8.4").
+Notation modulo := Nat.modulo (compat "8.4").
+Notation divmod_spec := Nat.divmod_spec (compat "8.4").
+Notation div_mod := Nat.div_mod (compat "8.4").
+Notation mod_bound_pos := Nat.mod_bound_pos (compat "8.4").
+Notation sqrt_iter := Nat.sqrt_iter (compat "8.4").
+Notation sqrt := Nat.sqrt (compat "8.4").
+Notation sqrt_iter_spec := Nat.sqrt_iter_spec (compat "8.4").
+Notation sqrt_spec := Nat.sqrt_spec (compat "8.4").
+Notation log2_iter := Nat.log2_iter (compat "8.4").
+Notation log2 := Nat.log2 (compat "8.4").
+Notation log2_iter_spec := Nat.log2_iter_spec (compat "8.4").
+Notation log2_spec := Nat.log2_spec (compat "8.4").
+Notation log2_nonpos := Nat.log2_nonpos (compat "8.4").
+Notation gcd := Nat.gcd (compat "8.4").
+Notation divide := Nat.divide (compat "8.4").
+Notation gcd_divide := Nat.gcd_divide (compat "8.4").
+Notation gcd_divide_l := Nat.gcd_divide_l (compat "8.4").
+Notation gcd_divide_r := Nat.gcd_divide_r (compat "8.4").
+Notation gcd_greatest := Nat.gcd_greatest (compat "8.4").
+Notation testbit := Nat.testbit (compat "8.4").
+Notation shiftl := Nat.shiftl (compat "8.4").
+Notation shiftr := Nat.shiftr (compat "8.4").
+Notation bitwise := Nat.bitwise (compat "8.4").
+Notation land := Nat.land (compat "8.4").
+Notation lor := Nat.lor (compat "8.4").
+Notation ldiff := Nat.ldiff (compat "8.4").
+Notation lxor := Nat.lxor (compat "8.4").
+Notation double_twice := Nat.double_twice (compat "8.4").
+Notation testbit_0_l := Nat.testbit_0_l (compat "8.4").
+Notation testbit_odd_0 := Nat.testbit_odd_0 (compat "8.4").
+Notation testbit_even_0 := Nat.testbit_even_0 (compat "8.4").
+Notation testbit_odd_succ := Nat.testbit_odd_succ (compat "8.4").
+Notation testbit_even_succ := Nat.testbit_even_succ (compat "8.4").
+Notation shiftr_spec := Nat.shiftr_spec (compat "8.4").
+Notation shiftl_spec_high := Nat.shiftl_spec_high (compat "8.4").
+Notation shiftl_spec_low := Nat.shiftl_spec_low (compat "8.4").
+Notation div2_bitwise := Nat.div2_bitwise (compat "8.4").
+Notation odd_bitwise := Nat.odd_bitwise (compat "8.4").
+Notation div2_decr := Nat.div2_decr (compat "8.4").
+Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (compat "8.4").
+Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (compat "8.4").
+Notation land_spec := Nat.land_spec (compat "8.4").
+Notation ldiff_spec := Nat.ldiff_spec (compat "8.4").
+Notation lor_spec := Nat.lor_spec (compat "8.4").
+Notation lxor_spec := Nat.lxor_spec (compat "8.4").
+
+Infix "<=?" := Nat.leb (at level 70) : nat_scope.
+Infix "<?" := Nat.ltb (at level 70) : nat_scope.
+Infix "^" := Nat.pow : nat_scope.
+Infix "/" := Nat.div : nat_scope.
+Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
+Notation "( x | y )" := (Nat.divide x y) (at level 0) : nat_scope.
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 4f3ffbcae..0bb7966d7 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -35,7 +35,7 @@ let explain_exn_default = function
(* Basic interaction exceptions *)
| Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
| Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
- | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
+ | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err))
| Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
| Out_of_memory -> hov 0 (str "Out of memory.")
| Stack_overflow -> hov 0 (str "Stack overflow.")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 063ed8964..040c33924 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -288,7 +288,7 @@ let rec discard_to_dot () =
try
Gram.entry_parse parse_to_dot top_buffer.tokens
with
- | Compat.Token.Error _ | Lexer.Error.E _ -> discard_to_dot ()
+ | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
| End_of_input -> raise End_of_input
| e when Errors.noncritical e -> ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c6f49dcd4..c4222b330 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -229,11 +229,11 @@ let compile_files () =
| [vf] -> compile_file vf (* One compilation : no need to save init state *)
| l ->
let init_state = States.freeze ~marshallable:`No in
- let coqdoc_init_state = Lexer.location_table () in
+ let coqdoc_init_state = CLexer.location_table () in
List.iter
(fun vf ->
States.unfreeze init_state;
- Lexer.restore_location_table coqdoc_init_state;
+ CLexer.restore_location_table coqdoc_init_state;
compile_file vf)
(List.rev l)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 701bc5da5..d60c73939 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -30,7 +30,7 @@ open Nameops
(**********************************************************************)
(* Tokens *)
-let cache_token (_,s) = Lexer.add_keyword s
+let cache_token (_,s) = CLexer.add_keyword s
let inToken : string -> obj =
declare_object {(default_object "TOKEN") with
@@ -272,7 +272,7 @@ let rec interp_list_parser hd = function
(* To protect alphabetic tokens and quotes from being seen as variables *)
let quote_notation_token x =
let n = String.length x in
- let norm = Lexer.is_ident x in
+ let norm = CLexer.is_ident x in
if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
else x
@@ -280,7 +280,7 @@ let rec raw_analyze_notation_tokens = function
| [] -> []
| String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
| String "_" :: _ -> error "_ must be quoted."
- | String x :: sl when Lexer.is_ident x ->
+ | String x :: sl when CLexer.is_ident x ->
NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
| String s :: sl ->
Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
@@ -569,7 +569,7 @@ let rec define_keywords_aux = function
| GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
when is_not_small_constr e ->
Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
- Lexer.add_keyword k;
+ CLexer.add_keyword k;
n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
| [] -> []
@@ -578,7 +578,7 @@ let rec define_keywords_aux = function
let define_keywords = function
| GramConstrTerminal(IDENT k)::l ->
Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
- Lexer.add_keyword k;
+ CLexer.add_keyword k;
GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l
@@ -607,12 +607,12 @@ let make_production etyps symbols =
let typ = List.assoc m etyps in
distribute [GramConstrNonTerminal (typ, Some m)] ll
| Terminal s ->
- distribute [GramConstrTerminal (Lexer.terminal s)] ll
+ distribute [GramConstrTerminal (CLexer.terminal s)] ll
| Break _ ->
ll
| SProdList (x,sl) ->
let tkl = List.flatten
- (List.map (function Terminal s -> [Lexer.terminal s]
+ (List.map (function Terminal s -> [CLexer.terminal s]
| Break _ -> []
| _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in
match List.assoc x etyps with
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b2fc456d0..54baa5e3c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -448,7 +448,7 @@ let subst_deps_obl obls obl =
let t' = subst_deps true obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
-module ProgMap = Map.Make(Id)
+module ProgMap = Id.Map
let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
@@ -698,11 +698,13 @@ let get_prog name =
match n with
0 -> raise (NoObligations None)
| 1 -> get_info (map_first prg_infos)
- | _ ->
- error ("More than one program with unsolved obligations: "^
- String.concat ", "
- (List.map string_of_id
- (ProgMap.fold (fun k _ s -> k::s) prg_infos []))))
+ | _ ->
+ let progs = Id.Set.elements (ProgMap.domain prg_infos) in
+ let prog = List.hd progs in
+ let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
+ errorlabstrm ""
+ (str "More than one program with unsolved obligations: " ++ progs
+ ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
let get_any_prog () =
let prg_infos = !from_prg in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1c8d60251..64225a644 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -162,17 +162,17 @@ let save_translator_coqdoc () =
(* translator state *)
let ch = !chan_beautify in
let cl = !Pp.comments in
- let cs = Lexer.com_state() in
+ let cs = CLexer.com_state() in
(* end translator state *)
- let coqdocstate = Lexer.location_table () in
+ let coqdocstate = CLexer.location_table () in
ch,cl,cs,coqdocstate
let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
if !Flags.beautify_file then close_out !chan_beautify;
chan_beautify := ch;
Pp.comments := cl;
- Lexer.restore_com_state cs;
- Lexer.restore_location_table coqdocstate
+ CLexer.restore_com_state cs;
+ CLexer.restore_location_table coqdocstate
(* For coqtop -time, we display the position in the file,
and a glimpse of the executed command *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 08:01:45 +0000