aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--configure.ml2
-rw-r--r--doc/faq/fk.bib2
-rw-r--r--doc/refman/RefMan-tac.tex9
-rw-r--r--doc/refman/RefMan-uti.tex2
-rw-r--r--doc/refman/biblio.bib2
-rw-r--r--engine/namegen.mli3
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--kernel/cbytecodes.ml20
-rw-r--r--kernel/cbytecodes.mli5
-rw-r--r--kernel/cbytegen.ml33
-rw-r--r--lib/cMap.ml6
-rw-r--r--lib/cMap.mli3
-rw-r--r--lib/hMap.ml101
-rw-r--r--ltac/profile_ltac.ml1
-rw-r--r--pretyping/pretyping.ml11
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/unification.ml3
-rw-r--r--proofs/refiner.ml2
-rw-r--r--test-suite/bugs/closed/4904.v11
-rw-r--r--toplevel/assumptions.ml4
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/vernac.ml19
-rw-r--r--toplevel/vernacentries.ml4
23 files changed, 180 insertions, 71 deletions
diff --git a/configure.ml b/configure.ml
index 13e1daedc..efba6f59b 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,7 +11,7 @@
#load "str.cma"
open Printf
-let coq_version = "trunk"
+let coq_version = "8.6.0"
let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of
three non-negative, period-separated integers [...]" *)
let vo_magic = 8511
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index 4d90efcdb..3410427de 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -2171,7 +2171,7 @@ Decomposition}},
@Misc{ProofGeneral,
author = {David Aspinall},
title = {Proof General},
- note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+ note = {\url{https://proofgeneral.github.io/}}
}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 21b72b8ef..b668239a6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2280,6 +2280,15 @@ hypothesis.
\end{Variants}
+\optindex{Structural Injection}
+
+It is possible to ensure that \texttt{injection {\term}} erases the
+original hypothesis and leaves the generated equalities in the context
+rather than putting them as antecedents of the current goal, as if
+giving \texttt{injection {\term} as} (with an empty list of names). To
+obtain this behavior, the option {\tt Set Structural Injection} must
+be activated. This option is off by default.
+
\subsection{\tt inversion \ident}
\tacindex{inversion}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c282083b5..10271ce0c 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
files.
{\ProofGeneral} is developed and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!.
\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 70ee1f41f..e69725838 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1199,7 +1199,7 @@ Decomposition}},
@Misc{ProofGeneral,
author = {David Aspinall},
title = {Proof General},
- note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+ note = {\url{https://proofgeneral.github.io/}}
}
@Book{CoqArt,
diff --git a/engine/namegen.mli b/engine/namegen.mli
index e5c156b4e..97c7c34a5 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -64,9 +64,6 @@ val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
but tolerate overwriting section variables, as in goals *)
val next_global_ident_away : Id.t -> Id.t list -> Id.t
-(** Avoid clashing with a constructor name already used in current module *)
-val next_name_away_in_cases_pattern : (Termops.names_context * constr) -> Name.t -> Id.t list -> Id.t
-
(** Default is [default_non_dependent_ident] *)
val next_name_away : Name.t -> Id.t list -> Id.t
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index f96d8acc1..d2dcbd92a 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -43,7 +43,7 @@ let is_alias_of_already_visible_name sp = function
false
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
- if not (is_alias_of_already_visible_name sp pat) then begin
+ if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
Nametab.push_syndef (Nametab.Exactly i) sp kn;
match onlyparse with
| None ->
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index a705e3004..8d4de523a 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -142,11 +142,29 @@ type fv = fv_elem array
exception NotClosed
+module Fv_elem =
+struct
+type t = fv_elem
+
+let compare e1 e2 = match e1, e2 with
+| FVnamed id1, FVnamed id2 -> Id.compare id1 id2
+| FVnamed _, _ -> -1
+| FVrel _, FVnamed _ -> 1
+| FVrel r1, FVrel r2 -> Int.compare r1 r2
+| FVrel _, FVuniv_var _ -> -1
+| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
+| FVuniv_var i1, _ -> 1
+
+end
+
+module FvMap = Map.Make(Fv_elem)
+
(*spiwack: both type have been moved from Cbytegen because I needed then
for the retroknowledge *)
type vm_env = {
size : int; (* longueur de la liste [n] *)
- fv_rev : fv_elem list (* [fvn; ... ;fv1] *)
+ fv_rev : fv_elem list; (* [fvn; ... ;fv1] *)
+ fv_fwd : int FvMap.t; (* reverse mapping *)
}
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 6fa0841af..5f1f09d00 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -139,11 +139,14 @@ type fv = fv_elem array
closed terms. *)
exception NotClosed
+module FvMap : Map.S with type key = fv_elem
+
(*spiwack: both type have been moved from Cbytegen because I needed them
for the retroknowledge *)
type vm_env = {
size : int; (** length of the list [n] *)
- fv_rev : fv_elem list (** [fvn; ... ;fv1] *)
+ fv_rev : fv_elem list; (** [fvn; ... ;fv1] *)
+ fv_fwd : int FvMap.t; (** reverse mapping *)
}
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 2d1ae68f4..008955d80 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -93,7 +93,12 @@ open Pre_env
type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
-let empty_fv = { size= 0; fv_rev = [] }
+let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty }
+let push_fv d e = {
+ size = e.size + 1;
+ fv_rev = d :: e.fv_rev;
+ fv_fwd = FvMap.add d e.size e.fv_fwd;
+}
let fv r = !(r.in_env)
@@ -184,20 +189,15 @@ let push_local sz r =
in_stack = (sz + 1) :: r.in_stack }
(*i Compilation of variables *)
-let find_at f l =
- let rec aux n = function
- | [] -> raise Not_found
- | hd :: tl -> if f hd then n else aux (n + 1) tl
- in aux 1 l
+let find_at fv env = FvMap.find fv env.fv_fwd
let pos_named id r =
let env = !(r.in_env) in
let cid = FVnamed id in
- let f = function FVnamed id' -> Id.equal id id' | _ -> false in
- try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
+ try Kenvacc(r.offset + find_at cid env)
with Not_found ->
let pos = env.size in
- r.in_env := { size = pos+1; fv_rev = cid:: env.fv_rev};
+ r.in_env := push_fv cid env;
Kenvacc (r.offset + pos)
let pos_rel i r sz =
@@ -212,11 +212,10 @@ let pos_rel i r sz =
let i = i - r.nb_rec in
let db = FVrel(i) in
let env = !(r.in_env) in
- let f = function FVrel j -> Int.equal i j | _ -> false in
- try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
+ try Kenvacc(r.offset + find_at db env)
with Not_found ->
let pos = env.size in
- r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
+ r.in_env := push_fv db env;
Kenvacc(r.offset + pos)
let pos_universe_var i r sz =
@@ -224,15 +223,11 @@ let pos_universe_var i r sz =
Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
else
let env = !(r.in_env) in
- let f = function
- | FVuniv_var u -> Int.equal i u
- | _ -> false
- in
- try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+ let db = FVuniv_var i in
+ try Kenvacc (r.offset + find_at db env)
with Not_found ->
let pos = env.size in
- let db = FVuniv_var i in
- r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ;
+ r.in_env := push_fv db env;
Kenvacc(r.offset + pos)
(*i Examination of the continuation *)
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 4b058380c..ba0873ffa 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -34,6 +34,7 @@ sig
val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a t -> 'a t
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+ val height : 'a t -> int
module Unsafe :
sig
val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
@@ -57,6 +58,7 @@ sig
val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a map -> 'a map
val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+ val height : 'a map -> int
module Unsafe :
sig
val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
@@ -168,6 +170,10 @@ struct
if l == l' && r == r' && v == v' then s
else map_inj (MNode (l', k, v', r', h))
+ let height s = match map_prj s with
+ | MEmpty -> 0
+ | MNode (_, _, _, _, h) -> h
+
module Unsafe =
struct
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 3ef7fa2c8..2838b374e 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -61,6 +61,9 @@ sig
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
(** As [mapi] but tries to preserve sharing. *)
+ val height : 'a t -> int
+ (** An indication of the logarithmic size of a map *)
+
module Unsafe :
sig
val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
diff --git a/lib/hMap.ml b/lib/hMap.ml
index 778c366fd..ea76e7427 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -68,34 +68,91 @@ struct
Int.Map.update h m s
with Not_found -> s
+ let height s = Int.Map.height s
+
+ let is_smaller s1 s2 = height s1 <= height s2 + 3
+
+ (** Assumes s1 << s2 *)
+ let fast_union s1 s2 =
+ let fold h s accu =
+ try Int.Map.modify h (fun _ s' -> Set.fold Set.add s s') accu
+ with Not_found -> Int.Map.add h s accu
+ in
+ Int.Map.fold fold s1 s2
+
let union s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | (Some _ as m), None | None, (Some _ as m) -> m
- | Some m1, Some m2 -> Some (Set.union m1 m2)
+ if is_smaller s1 s2 then fast_union s1 s2
+ else if is_smaller s2 s1 then fast_union s2 s1
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None | None, (Some _ as m) -> m
+ | Some m1, Some m2 -> Some (Set.union m1 m2)
+ in
+ Int.Map.merge fu s1 s2
+
+ (** Assumes s1 << s2 *)
+ let fast_inter s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h s2 in
+ let si = Set.filter (fun e -> Set.mem e s') s in
+ if Set.is_empty si then accu
+ else Int.Map.add h si accu
+ with Not_found -> accu
in
- Int.Map.merge fu s1 s2
+ Int.Map.fold fold s1 Int.Map.empty
let inter s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | Some _, None | None, Some _ -> None
- | Some m1, Some m2 ->
- let m = Set.inter m1 m2 in
- if Set.is_empty m then None else Some m
+ if is_smaller s1 s2 then fast_inter s1 s2
+ else if is_smaller s2 s1 then fast_inter s2 s1
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | Some _, None | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.inter m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
+
+ (** Assumes s1 << s2 *)
+ let fast_diff_l s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h s2 in
+ let si = Set.filter (fun e -> not (Set.mem e s')) s in
+ if Set.is_empty si then accu
+ else Int.Map.add h si accu
+ with Not_found -> Int.Map.add h s accu
+ in
+ Int.Map.fold fold s1 Int.Map.empty
+
+ (** Assumes s2 << s1 *)
+ let fast_diff_r s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h accu in
+ let si = Set.filter (fun e -> not (Set.mem e s)) s' in
+ if Set.is_empty si then Int.Map.remove h accu
+ else Int.Map.update h si accu
+ with Not_found -> accu
in
- Int.Map.merge fu s1 s2
+ Int.Map.fold fold s2 s1
let diff s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | (Some _ as m), None -> m
- | None, Some _ -> None
- | Some m1, Some m2 ->
- let m = Set.diff m1 m2 in
- if Set.is_empty m then None else Some m
- in
- Int.Map.merge fu s1 s2
+ if is_smaller s1 s2 then fast_diff_l s1 s2
+ else if is_smaller s2 s2 then fast_diff_r s1 s2
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None -> m
+ | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.diff m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
let compare s1 s2 = Int.Map.compare Set.compare s1 s2
@@ -324,6 +381,8 @@ struct
let fs m = Map.smartmapi f m in
Int.Map.smartmap fs s
+ let height s = Int.Map.height s
+
module Unsafe =
struct
let map f s =
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index bea02e3dc..fb71becfc 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -235,7 +235,6 @@ let rec print_node all_total indent prefix (s, n) =
++ padl 8 (string_of_int e.ncalls)
++ padl 10 (format_sec (e.max_total))
) ++
- fnl () ++
print_table all_total indent false n.children
and print_table all_total indent first_level table =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a172d2560..0f85dc629 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -404,9 +404,10 @@ let ltac_interp_name_env k0 lvar env =
(* tail is the part of the env enriched by pretyping *)
let n = Context.Rel.length (rel_context env) - k0 in
let ctxt,_ = List.chop n (rel_context env) in
- let env = pop_rel_context n env in
- let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in
- push_rel_context ctxt env
+ let open Context.Rel.Declaration in
+ let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
+ if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
+ else push_rel_context ctxt' (pop_rel_context n env)
let invert_ltac_bound_name lvar env id0 id =
let id' = Id.Map.find id lvar.ltac_idents in
@@ -804,8 +805,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = pretype_type empty_valcon env evdref lvar c2 in
{ j with utj_val = lift 1 j.utj_val }
| Name _ ->
- let var = (name,j.utj_val) in
- let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in
+ let var = LocalAssum (name, j.utj_val) in
+ let env' = push_rel var env in
pretype_type empty_valcon env' evdref lvar c2
in
let name = ltac_interp_name lvar name in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5484e70b6..8259876c2 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -790,11 +790,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
(h 0 (str "<<" ++ Termops.print_constr x ++
str "|" ++ cut () ++ Cst_stack.pr cst_l ++
str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
- str ">>") ++ fnl ())
+ str ">>"))
in
let fold () =
let () = if !debug_RAKAM then
- let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in
+ let open Pp in Feedback.msg_notice (str "<><><><><>") in
(s,cst_l)
in
match kind_of_term x with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e9ee55d37..213eecc6b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1081,8 +1081,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
a
with e ->
+ let e = CErrors.push e in
if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
- raise e
+ iraise e
let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index d9ab2fbdb..fdd0df445 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -222,7 +222,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
Feedback.msg_notice
(str (emacs_str "<infoH>")
++ (hov 0 (str s))
- ++ (str (emacs_str "</infoH>")) ++ fnl());
+ ++ (str (emacs_str "</infoH>")));
tclIDTAC goal;;
diff --git a/test-suite/bugs/closed/4904.v b/test-suite/bugs/closed/4904.v
new file mode 100644
index 000000000..a47c3b07a
--- /dev/null
+++ b/test-suite/bugs/closed/4904.v
@@ -0,0 +1,11 @@
+Module A.
+Module B.
+Notation mynat := nat.
+Notation nat := nat.
+End B.
+End A.
+
+Print A.B.nat. (* Notation A.B.nat := nat *)
+Import A.
+Print B.mynat.
+Print B.nat.
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 9a7ea3cde..49a815dc1 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -285,7 +285,9 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let fold obj _ accu = match obj with
| VarRef id ->
let decl = Global.lookup_named id in
- if is_local_assum decl then ContextObjectMap.add (Variable id) t accu
+ if is_local_assum decl then
+ let t = Context.Named.Declaration.get_type decl in
+ ContextObjectMap.add (Variable id) t accu
else accu
| ConstRef kn ->
let cb = lookup_constant kn in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c49a97cad..a56459f18 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -382,7 +382,7 @@ let get_host_port opt s =
Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
| ["stdfds"] -> Some Spawned.AnonPipe
| _ ->
- prerr_endline ("Error: host:port or stdfds expected after option "^opt);
+ prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt);
exit 1
let get_error_resilience opt = function
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f83ada466..6dba2c51e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -101,7 +101,7 @@ let verbose_phrase verbch loc =
let s = String.create len in
seek_in ch (fst loc);
really_input ch s 0 len;
- Feedback.msg_notice (str s ++ fnl ())
+ Feedback.msg_notice (str s)
| None -> ()
exception End_of_input
@@ -158,7 +158,7 @@ let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
(* For coqtop -time, we display the position in the file,
and a glimpse of the executed command *)
-let display_cmd_header loc com =
+let pp_cmd_header loc com =
let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
let noblank s =
for i = 0 to String.length s - 1 do
@@ -173,11 +173,15 @@ let display_cmd_header loc com =
try Ppvernac.pr_vernac x
with e -> str (Printexc.to_string e) in
let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
- in
- Feedback.msg_notice
- (str "Chars " ++ int start ++ str " - " ++ int stop ++
- str " [" ++ str cmd ++ str "] ")
+ in str "Chars " ++ int start ++ str " - " ++ int stop ++
+ str " [" ++ str cmd ++ str "] "
+(* This is a special case where we assume we are in console batch mode
+ and take control of the console.
+ *)
+let print_cmd_header loc com =
+ Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
+ Format.pp_print_flush !Pp_control.std_ft ()
let rec vernac_com checknav (loc,com) =
let interp = function
@@ -208,7 +212,8 @@ let rec vernac_com checknav (loc,com) =
try
checknav loc com;
if do_beautify () then pr_new_syntax loc (Some com);
- if !Flags.time then display_cmd_header loc com;
+ (* XXX: This is not 100% correct if called from an IDE context *)
+ if !Flags.time then print_cmd_header loc com;
let com = if !Flags.time then VernacTime (loc,com) else com in
let a = CLexer.com_state () in
interp com;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5b746ca46..eeb4e26af 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -137,7 +137,7 @@ let make_cases s =
let rec rename avoid = function
| [] -> []
| (n,_)::l ->
- let n' = Namegen.next_name_away_in_cases_pattern ([],mkMeta 0) n avoid in
+ let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
Id.to_string n' :: rename (n'::avoid) l in
let al' = rename [] al in
(Id.to_string consname :: al') :: l)
@@ -1065,7 +1065,7 @@ let vernac_declare_arguments locality r l nargs flags =
vernac_declare_implicits locality r []
else if some_implicits_specified || List.mem `ClearImplicits flags then
vernac_declare_implicits locality r implicits;
- if nargs >= 0 && nargs < List.fold_left max 0 rargs then
+ if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then
error "The \"/\" option must be placed after the last \"!\".";
let no_flags = List.is_empty flags in
let rec narrow = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 10:42:42 +0000