diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-25 14:31:30 +0200 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-25 14:31:30 +0200 |
commit | a2b0c48d8b531ae1b193eed4dec1afeaa67fbece (patch) | |
tree | af83d8a0fb79c51e13c44bc60be9cde810f87152 | |
parent | 1297523bffdc3a9fe3e447acc6837be835e86d06 (diff) | |
parent | 7244637f251272c0d0155d49fc7c1af255b7cef8 (diff) |
Merge remote-tracking branch 'v8.6' into trunk
-rw-r--r-- | configure.ml | 2 | ||||
-rw-r--r-- | doc/faq/fk.bib | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 9 | ||||
-rw-r--r-- | doc/refman/RefMan-uti.tex | 2 | ||||
-rw-r--r-- | doc/refman/biblio.bib | 2 | ||||
-rw-r--r-- | engine/namegen.mli | 3 | ||||
-rw-r--r-- | interp/syntax_def.ml | 2 | ||||
-rw-r--r-- | kernel/cbytecodes.ml | 20 | ||||
-rw-r--r-- | kernel/cbytecodes.mli | 5 | ||||
-rw-r--r-- | kernel/cbytegen.ml | 33 | ||||
-rw-r--r-- | lib/cMap.ml | 6 | ||||
-rw-r--r-- | lib/cMap.mli | 3 | ||||
-rw-r--r-- | lib/hMap.ml | 101 | ||||
-rw-r--r-- | ltac/profile_ltac.ml | 1 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 11 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
-rw-r--r-- | pretyping/unification.ml | 3 | ||||
-rw-r--r-- | proofs/refiner.ml | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4904.v | 11 | ||||
-rw-r--r-- | toplevel/assumptions.ml | 4 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
-rw-r--r-- | toplevel/vernac.ml | 19 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 4 |
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 |