aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xdev/bench/render_results322
-rwxr-xr-xdev/lint-repository.sh6
-rw-r--r--interp/constrextern.ml14
-rw-r--r--kernel/cClosure.ml58
-rw-r--r--plugins/extraction/mlutil.ml6
-rw-r--r--test-suite/bugs/closed/bug_13453.v6
-rw-r--r--test-suite/bugs/closed/bug_7967.v4
-rw-r--r--test-suite/output/Notations4.out22
-rw-r--r--test-suite/output/Notations4.v44
-rw-r--r--test-suite/output/NotationsCoercions.out22
-rw-r--r--test-suite/output/NotationsCoercions.v77
-rw-r--r--vernac/comAssumption.ml5
12 files changed, 340 insertions, 246 deletions
diff --git a/dev/bench/render_results b/dev/bench/render_results
index 72affd70b2..bd4308837b 100755
--- a/dev/bench/render_results
+++ b/dev/bench/render_results
@@ -76,25 +76,13 @@ let run_and_read cmd =
;;
let ( %> ) f g x = g (f x)
-;;
let run = run_and_read %> snd
-;;
module Float = struct
let nan = Pervasives.nan
end
-module Tuple4 = struct
-
- let first (x,_,_,_) = x
- let second (_,y,_,_) = y
- let third (_,_,z,_) = z
- let fourth (_,_,_,z) = z
-
-end
-;;
-
module List = struct
include List
@@ -149,6 +137,151 @@ module String = struct
end
;;
+module Table :
+sig
+ type header = string
+ type row = string list list
+ val print : header list -> row list -> string
+end =
+struct
+ type header = string
+
+ type row = string list list
+
+ let val_padding = 2
+ (* Padding between data in the same row *)
+ let row_padding = 1
+ (* Padding between rows *)
+
+ let homogeneous b = if b then () else failwith "Heterogeneous data"
+
+ let vert_split (ls : 'a list list) =
+ let split l = match l with
+ | [] -> failwith "vert_split"
+ | x :: l -> (x, l)
+ in
+ let ls = List.map split ls in
+ List.split ls
+
+ let rec last = function
+ | [] -> assert false
+ | [x] -> [], x
+ | x :: l ->
+ let (l, y) = last l in
+ (x :: l, y)
+
+ let justify n s =
+ let len = String.length s in
+ let () = assert (len <= n) in
+ let lft = (n - len) / 2 in
+ let rgt = n - lft - len in
+ String.make lft ' ' ^ s ^ String.make rgt ' '
+
+ let justify_row layout data =
+ let map n s =
+ let len = String.length s in
+ let () = assert (len <= n) in
+ (* Right align *)
+ let pad = n - len in
+ String.make pad ' ' ^ s
+ in
+ let data = List.map2 map layout data in
+ String.concat (String.make val_padding ' ') data
+
+ let angle hkind vkind = match hkind, vkind with
+ | `Lft, `Top -> "┌"
+ | `Rgt, `Top -> "┐"
+ | `Mid, `Top -> "┬"
+ | `Lft, `Mid -> "├"
+ | `Rgt, `Mid -> "┤"
+ | `Mid, `Mid -> "┼"
+ | `Lft, `Bot -> "└"
+ | `Rgt, `Bot -> "┘"
+ | `Mid, `Bot -> "┴"
+
+ let print_separator vkind col_size =
+ let rec dashes n = if n = 0 then "" else "─" ^ dashes (n - 1) in
+ let len = List.length col_size in
+ let pad = dashes row_padding in
+ let () = assert (0 < len) in
+ let map n = dashes n in
+ angle `Lft vkind ^ pad ^
+ String.concat (pad ^ angle `Mid vkind ^ pad) (List.map map col_size) ^
+ pad ^ angle `Rgt vkind
+
+ let print_blank col_size =
+ let len = List.length col_size in
+ let () = assert (0 < len) in
+ let pad = String.make row_padding ' ' in
+ let map n = String.make n ' ' in
+ "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) (List.map map col_size) ^ pad ^ "│"
+
+ let print_row row =
+ let len = List.length row in
+ let () = assert (0 < len) in
+ let pad = String.make row_padding ' ' in
+ "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) row ^ pad ^ "│"
+
+ (* Invariant : all rows must have the same shape *)
+
+ let print (headers : header list) (rows : row list) =
+ (* Sanitize input *)
+ let ncolums = List.length headers in
+ let shape = ref None in
+ let check row =
+ let () = homogeneous (List.length row = ncolums) in
+ let rshape : int list = List.map (fun data -> List.length data) row in
+ match !shape with
+ | None -> shape := Some rshape
+ | Some s -> homogeneous (rshape = s)
+ in
+ let () = List.iter check rows in
+ (* Compute layout *)
+ let rec layout n (rows : row list) =
+ if n = 0 then []
+ else
+ let (col, rows) = vert_split rows in
+ let ans = layout (n - 1) rows in
+ let data = ref None in
+ let iter args =
+ let size = List.map String.length args in
+ match !data with
+ | None -> data := Some size
+ | Some s ->
+ data := Some (List.map2 (fun len1 len2 -> max len1 len2) s size)
+ in
+ let () = List.iter iter col in
+ let data = match !data with None -> [] | Some s -> s in
+ data :: ans
+ in
+ let layout = layout ncolums rows in
+ let map hd shape =
+ let data_size = match shape with
+ | [] -> 0
+ | n :: shape -> List.fold_left (fun accu n -> accu + n + val_padding) n shape
+ in
+ max (String.length hd) data_size
+ in
+ let col_size = List.map2 map headers layout in
+ (* Justify the data *)
+ let headers = List.map2 justify col_size headers in
+ let rows = List.map (fun row -> List.map2 justify col_size (List.map2 justify_row layout row)) rows in
+ (* Print the table *)
+ let rows, last = last rows in
+ let sep = print_separator `Mid col_size in
+ let rows = List.concat @@ List.map (fun r -> [print_row r; sep]) rows in
+ let lines =
+ print_separator `Top col_size ::
+ print_row headers ::
+ print_blank col_size ::
+ rows @
+ print_row last ::
+ print_separator `Bot col_size ::
+ []
+ in
+ String.concat "\n" lines
+end
+
(******************************************************************************)
(* END Copied from batteries, to remove *)
(******************************************************************************)
@@ -203,10 +336,6 @@ let proportional_difference_of_integers new_value old_value =
else float_of_int (new_value - old_value) /. float_of_int old_value *. 100.0
in
-let count_number_of_digits_before_decimal_point =
- log10 %> floor %> int_of_float %> succ %> max 1
-in
-
(* parse the *.time and *.perf files *)
coq_opam_packages
|> List.map
@@ -259,138 +388,39 @@ coq_opam_packages
(* Below we take the measurements and format them to stdout. *)
+|> List.map begin fun (package_name, new_t, old_t, perc) ->
+
+ let precision = 2 in
+ let prf f = Printf.sprintf "%.*f" precision f in
+ let pri n = Printf.sprintf "%d" n in
+
+ [
+ [ package_name ];
+ [ prf new_t.user_time; prf old_t.user_time; prf perc.user_time ];
+ [ pri new_t.num_cycles; pri old_t.num_cycles; prf perc.num_cycles ];
+ [ pri new_t.num_instr; pri old_t.num_instr; prf perc.num_instr ];
+ [ pri new_t.num_mem; pri old_t.num_mem; prf perc.num_mem ];
+ [ pri new_t.num_faults; pri old_t.num_faults; prf perc.num_faults ];
+ ]
+
+ end
+
|> fun measurements ->
- let precision = 2 in
-
- (* the labels that we will print *)
- let package_name__label = "package_name" in
- let new__label = "NEW" in
- let old__label = "OLD" in
- let proportional_difference__label = "PDIFF" in
-
- (* the lengths of labels that we will print *)
- let new__label__length = String.length new__label in
- let proportional_difference__label__length = String.length proportional_difference__label in
-
- (* widths of individual columns of the table *)
- let package_name__width =
- max (measurements |> List.map (Tuple4.first %> String.length) |> List.max)
- (String.length package_name__label) in
-
- let llf proj =
- let lls = count_number_of_digits_before_decimal_point (List.max proj) + 1 + precision in
- max lls new__label__length in
-
- let lli proj =
- let lls = count_number_of_digits_before_decimal_point (float_of_int (List.(max proj))) + 1 + precision in
- max lls new__label__length in
-
- let new_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.second measurements in
- let old_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.third measurements in
-
- let llp proj =
- let lls =
- count_number_of_digits_before_decimal_point List.(max List.(map abs_float proj)) + 2 + precision in
- max lls proportional_difference__label__length in
-
- let perc_timing_width = reduce_pkg_timings llp llp @@ List.map Tuple4.fourth measurements in
-
- (* print the table *)
- let rec make_dashes = function
- | 0 -> ""
- | count -> "─" ^ make_dashes (pred count)
- in
-
- let vertical_separator left_glyph middle_glyph right_glyph =
- sprintf "%s─%s─%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s\n"
- left_glyph
- (make_dashes package_name__width)
- middle_glyph
- (make_dashes new_timing_width.user_time)
- (make_dashes old_timing_width.user_time)
- (make_dashes perc_timing_width.user_time)
- middle_glyph
- (make_dashes new_timing_width.num_cycles)
- (make_dashes old_timing_width.num_cycles)
- (make_dashes perc_timing_width.num_cycles)
- middle_glyph
- (make_dashes new_timing_width.num_instr)
- (make_dashes old_timing_width.num_instr)
- (make_dashes perc_timing_width.num_instr)
- middle_glyph
- (make_dashes new_timing_width.num_mem)
- (make_dashes old_timing_width.num_mem)
- (make_dashes perc_timing_width.num_mem)
- middle_glyph
- (make_dashes new_timing_width.num_faults)
- (make_dashes old_timing_width.num_faults)
- (make_dashes perc_timing_width.num_faults)
- right_glyph
- in
-
- let center_string string width =
- let string_length = String.length string in
- let width = max width string_length in
- let left_hfill = (width - string_length) / 2 in
- let right_hfill = width - left_hfill - string_length in
- String.make left_hfill ' ' ^ string ^ String.make right_hfill ' '
- in
- printf "\n";
- print_string (vertical_separator "┌" "┬" "┐");
- "│" ^ String.make (1 + package_name__width + 1) ' ' ^ "│"
- ^ center_string "user time [s]" (1 + new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) ^ "│"
- ^ center_string "CPU cycles" (1 + new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) ^ "│"
- ^ center_string "CPU instructions" (1 + new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ^ "│"
- ^ center_string "max resident mem [KB]" (1 + new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ^ "│"
- ^ center_string "mem faults" (1 + new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3)
- ^ "│\n" |> print_string;
- printf "│%*s │ %*s│ %*s│ %*s│ %*s│ %*s│\n"
- (1 + package_name__width) ""
- (new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) ""
- (new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) ""
- (new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ""
- (new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ""
- (new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) "";
- printf "│ %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │\n"
- package_name__width package_name__label
- new_timing_width.user_time new__label
- old_timing_width.user_time old__label
- perc_timing_width.user_time proportional_difference__label
- new_timing_width.num_cycles new__label
- old_timing_width.num_cycles old__label
- perc_timing_width.num_cycles proportional_difference__label
- new_timing_width.num_instr new__label
- old_timing_width.num_instr old__label
- perc_timing_width.num_instr proportional_difference__label
- new_timing_width.num_mem new__label
- old_timing_width.num_mem old__label
- perc_timing_width.num_mem proportional_difference__label
- new_timing_width.num_faults new__label
- old_timing_width.num_faults old__label
- perc_timing_width.num_faults proportional_difference__label;
- measurements |> List.iter
- (fun (package_name, new_t, old_t, perc) ->
- print_string (vertical_separator "├" "┼" "┤");
- printf "│ %*s │ %*.*f %*.*f %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │\n"
- package_name__width package_name
- new_timing_width.user_time precision new_t.user_time
- old_timing_width.user_time precision old_t.user_time
- perc_timing_width.user_time precision perc.user_time
- new_timing_width.num_cycles new_t.num_cycles
- old_timing_width.num_cycles old_t.num_cycles
- perc_timing_width.num_cycles precision perc.num_cycles
- new_timing_width.num_instr new_t.num_instr
- old_timing_width.num_instr old_t.num_instr
- perc_timing_width.num_instr precision perc.num_instr
- new_timing_width.num_mem new_t.num_mem
- old_timing_width.num_mem old_t.num_mem
- perc_timing_width.num_mem precision perc.num_mem
- new_timing_width.num_faults new_t.num_faults
- old_timing_width.num_faults old_t.num_faults
- perc_timing_width.num_faults precision perc.num_faults);
-
-print_string (vertical_separator "└" "┴" "┘");
+ let headers = [
+ "";
+ "user time [s]";
+ "CPU cycles";
+ "CPU instructions";
+ "max resident mem [KB]";
+ "mem faults";
+ ] in
+
+ let descr = ["NEW"; "OLD"; "PDIFF"] in
+ let top = [ [ "package_name" ]; descr; descr; descr; descr; descr ] in
+
+ printf "%s%!" (Table.print headers (top :: measurements))
+;
(* ejgallego: disable this as it is very verbose and brings up little info in the log. *)
if false then begin
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 2e8a7455de..7701264ad1 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -9,10 +9,10 @@
CODE=0
-if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then
- # The FIRST parent of bot merges is from the PR, the second is
+if [[ $(git log -n 1 --pretty='format:%s') == "[CI merge]"* ]]; then
+ # The second parent of bot merges is from the PR, the first is
# current master
- head=$(git rev-parse HEAD~)
+ head=$(git rev-parse HEAD^2)
else
head=$(git rev-parse HEAD)
fi
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cf88036f73..378adb566c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -800,19 +800,21 @@ let extern_args extern env args =
let match_coercion_app c = match DAst.get c with
| GApp (r, args) ->
begin match DAst.get r with
- | GRef (r,_) -> Some (c.CAst.loc, r, 0, args)
+ | GRef (r,_) -> Some (c.CAst.loc, r, args)
| _ -> None
end
| _ -> None
let remove_one_coercion inctx c =
try match match_coercion_app c with
- | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
+ | Some (loc,r,args) when not (!Flags.raw_print || !print_coercions) ->
let nargs = List.length args in
(match Coercionops.hide_coercion r with
- | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
+ | Some nparams when
+ let inctx = inctx || (* coercion to funclass implying being in context *) nparams+1 < nargs in
+ nparams < nargs && inctx ->
(* We skip the coercion *)
- let l = List.skipn (n - pars) args in
+ let l = List.skipn nparams args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
(* Don't flatten App's in case of funclass so that
(atomic) notations on [a] work; should be compatible
@@ -824,7 +826,7 @@ let remove_one_coercion inctx c =
have been made explicit to match *)
let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in
let inctx = inctx || not (List.is_empty l) in
- Some (n-pars+1, inctx, a')
+ Some (nparams+1, inctx, a')
| _ -> None)
| _ -> None
with Not_found ->
@@ -867,7 +869,7 @@ let filter_enough_applied nargs l =
| Some nargs ->
List.filter (fun (keyrule,pat,n as _rule) ->
match n with
- | AppBoundedNotation n -> n > nargs
+ | AppBoundedNotation n -> n >= nargs
| AppUnboundedNotation | NotAppNotation -> false) l
(* Helper function for safe and optimal printing of primitive tokens *)
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 17feeb9b5a..c9326615dc 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -263,7 +263,7 @@ let assoc_defined id env = match Environ.lookup_named id env with
* before the term is computed.
*)
-(* Norm means the term is fully normalized and cannot create a redex
+(* Ntrl means the term is fully normalized and cannot create a redex
when substituted
Cstr means the term is in head normal form and that it can
create a redex when substituted (i.e. constructor, fix, lambda)
@@ -271,10 +271,10 @@ let assoc_defined id env = match Environ.lookup_named id env with
create a redex when substituted
Red is used for terms that might be reduced
*)
-type red_state = Norm | Cstr | Whnf | Red
+type red_state = Ntrl | Cstr | Whnf | Red
let neutr = function
- | Whnf|Norm -> Whnf
+ | Whnf|Ntrl -> Whnf
| Red|Cstr -> Red
type optrel = Unknown | KnownR | KnownI
@@ -293,13 +293,13 @@ module Mark : sig
val neutr : t -> t
- val set_norm : t -> t
+ val set_ntrl : t -> t
end = struct
type t = int
let[@inline] of_state = function
- | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11
+ | Ntrl -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11
let[@inline] of_relevance = function
| Unknown -> 0
@@ -315,15 +315,15 @@ end = struct
| _ -> assert false
let[@inline] red_state x = match x land 0b1100 with
- | 0b0000 -> Norm
+ | 0b0000 -> Ntrl
| 0b0100 -> Cstr
| 0b1000 -> Whnf
| 0b1100 -> Red
| _ -> assert false
- let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *)
+ let[@inline] neutr x = x lor 0b1000 (* Whnf|Ntrl -> Whnf | Red|Cstr -> Red *)
- let[@inline] set_norm x = x land 0b0011
+ let[@inline] set_ntrl x = x land 0b0011
end
let mark = Mark.mark
@@ -358,10 +358,10 @@ and fterm =
and finvert = Univ.Instance.t * fconstr array
let fterm_of v = v.term
-let set_norm v = v.mark <- Mark.set_norm v.mark
-let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false
+let set_ntrl v = v.mark <- Mark.set_ntrl v.mark
+let is_val v = match Mark.red_state v.mark with Ntrl -> true | Cstr | Whnf | Red -> false
-let mk_atom c = {mark=mark Norm Unknown;term=FAtom c}
+let mk_atom c = {mark=mark Ntrl Unknown;term=FAtom c}
let mk_red f = {mark=mark Red Unknown;term=f}
(* Could issue a warning if no is still Red, pointing out that we loose
@@ -448,7 +448,7 @@ let rec lft_fconstr n ft =
let r = Mark.relevance ft.mark in
match ft.term with
| (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft
- | FRel i -> {mark=mark Norm r;term=FRel(i+n)}
+ | FRel i -> {mark=mark Ntrl r;term=FRel(i+n)}
| FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))}
| FFix(fx,e) ->
{mark=mark Cstr r; term=FFix(fx,subs_shft(n,e))}
@@ -466,7 +466,7 @@ let lift_fconstr_vect k v =
let clos_rel e i =
match expand_rel i e with
| Inl(n,mt) -> lift_fconstr n mt
- | Inr(k,None) -> {mark=mark Norm Unknown; term= FRel k}
+ | Inr(k,None) -> {mark=mark Ntrl Unknown; term= FRel k}
| Inr(k,Some p) ->
lift_fconstr (k-p) {mark=mark Red Unknown;term=FFlex(RelKey p)}
@@ -488,7 +488,7 @@ let compact_stack head stk =
(* Put an update mark in the stack, only if needed *)
let zupdate info m s =
let share = info.i_cache.i_share in
- if share && begin match Mark.red_state m.mark with Red -> true | Norm | Whnf | Cstr -> false end
+ if share && begin match Mark.red_state m.mark with Red -> true | Ntrl | Whnf | Cstr -> false end
then
let s' = compact_stack m s in
let _ = m.term <- FLOCKED in
@@ -514,8 +514,8 @@ let mk_clos e t =
| Rel i -> clos_rel e i
| Var x -> {mark = mark Red Unknown; term = FFlex (VarKey x) }
| Const c -> {mark = mark Red Unknown; term = FFlex (ConstKey c) }
- | Meta _ | Sort _ -> {mark = mark Norm KnownR; term = FAtom t }
- | Ind kn -> {mark = mark Norm KnownR; term = FInd kn }
+ | Meta _ | Sort _ -> {mark = mark Ntrl KnownR; term = FAtom t }
+ | Ind kn -> {mark = mark Ntrl KnownR; term = FInd kn }
| Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn }
| Int i -> {mark = mark Cstr Unknown; term = FInt i}
| Float f -> {mark = mark Cstr Unknown; term = FFloat f}
@@ -734,11 +734,11 @@ let strip_update_shift_app_red head stk =
strip_rec [] head 0 stk
let strip_update_shift_app head stack =
- assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true);
+ assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true);
strip_update_shift_app_red head stack
let get_nth_arg head n stk =
- assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true);
+ assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true);
let rec strip_rec rstk h n = function
| Zshift(k) as e :: s ->
strip_rec (e::rstk) (lift_fconstr k h) n s
@@ -787,7 +787,7 @@ let rec eta_expand_stack = function
| Zshift _ | Zupdate _ | Zprimitive _ as e) :: s ->
e :: eta_expand_stack s
| [] ->
- [Zshift 1; Zapp [|{mark=mark Norm Unknown; term= FRel 1}|]]
+ [Zshift 1; Zapp [|{mark=mark Ntrl Unknown; term= FRel 1}|]]
(* Get the arguments of a native operator *)
let rec skip_native_args rargs nargs =
@@ -968,7 +968,7 @@ module FNativeEntries =
| FArray (_u,t,_ty) -> t
| _ -> raise Not_found
- let dummy = {mark = mark Norm KnownR; term = FRel 0}
+ let dummy = {mark = mark Ntrl KnownR; term = FRel 0}
let current_retro = ref Retroknowledge.empty
let defined_int = ref false
@@ -978,7 +978,7 @@ module FNativeEntries =
match retro.Retroknowledge.retro_int63 with
| Some c ->
defined_int := true;
- fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+ fint := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
| None -> defined_int := false
let defined_float = ref false
@@ -988,7 +988,7 @@ module FNativeEntries =
match retro.Retroknowledge.retro_float64 with
| Some c ->
defined_float := true;
- ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+ ffloat := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
| None -> defined_float := false
let defined_bool = ref false
@@ -1039,7 +1039,7 @@ module FNativeEntries =
fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) };
fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) };
let (icmp, _) = cEq in
- fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) }
+ fcmp := { mark = mark Ntrl KnownR; term = FInd (Univ.in_punivs icmp) }
| None -> defined_cmp := false
let defined_f_cmp = ref false
@@ -1327,19 +1327,19 @@ let rec knr info tab m stk =
let rargs, a, nargs, stk = get_native_args1 op c stk in
kni info tab a (Zprimitive(op,c,rargs,nargs)::stk)
else
- (* Similarly to fix, partially applied primitives are not Norm! *)
+ (* Similarly to fix, partially applied primitives are not Ntrl! *)
(m, stk)
- | Undef _ | OpaqueDef _ -> (set_norm m; (m,stk)))
+ | Undef _ | OpaqueDef _ -> (set_ntrl m; (m,stk)))
| FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
(match ref_value_cache info tab (VarKey id) with
| Def v -> kni info tab v stk
| Primitive _ -> assert false
- | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk)))
+ | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk)))
| FFlex(RelKey k) when red_set info.i_flags fDELTA ->
(match ref_value_cache info tab (RelKey k) with
| Def v -> kni info tab v stk
| Primitive _ -> assert false
- | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk)))
+ | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk)))
| FConstruct((_ind,c),_u) ->
let use_match = red_set info.i_flags fMATCH in
let use_fix = red_set info.i_flags fFIX in
@@ -1523,9 +1523,9 @@ let norm_val info tab v =
with_stats (lazy (kl info tab v))
let whd_stack infos tab m stk = match Mark.red_state m.mark with
-| Whnf | Norm ->
+| Whnf | Ntrl ->
(** No need to perform [kni] nor to unlock updates because
- every head subterm of [m] is [Whnf] or [Norm] *)
+ every head subterm of [m] is [Whnf] or [Ntrl] *)
knh infos m stk
| Red | Cstr ->
let k = kni infos tab m stk in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 21ec80abbc..da4a50b674 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -399,7 +399,11 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
| MLuint i1, MLuint i2 -> Uint63.equal i1 i2
| MLfloat f1, MLfloat f2 -> Float64.equal f1 f2
-| _, _ -> false
+| MLparray (t1,def1), MLparray (t2, def2) -> Array.equal eq_ml_ast t1 t2 && eq_ml_ast def1 def2
+| (MLrel _|MLapp _|MLlam _|MLletin _|MLglob _|MLcons _
+ |MLtuple _|MLcase _|MLfix _|MLexn _|MLdummy _|MLaxiom
+ | MLmagic _| MLuint _| MLfloat _|MLparray _), _
+ -> false
and eq_ml_pattern p1 p2 = match p1, p2 with
| Pcons (gr1, p1), Pcons (gr2, p2) ->
diff --git a/test-suite/bugs/closed/bug_13453.v b/test-suite/bugs/closed/bug_13453.v
new file mode 100644
index 0000000000..4d0e435df7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13453.v
@@ -0,0 +1,6 @@
+Require Extraction.
+
+Primitive array := #array_type.
+
+Definition a : array nat := [| 0%nat | 0%nat |].
+Extraction a.
diff --git a/test-suite/bugs/closed/bug_7967.v b/test-suite/bugs/closed/bug_7967.v
index 2c8855fd54..987a820831 100644
--- a/test-suite/bugs/closed/bug_7967.v
+++ b/test-suite/bugs/closed/bug_7967.v
@@ -1,2 +1,6 @@
Set Universe Polymorphism.
Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A.
+
+(* A similar bug *)
+Context (C := ltac:(let y := constr:(Type) in exact nat)).
+Check C@{}.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index df64ae2af3..3477a293e3 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -31,12 +31,6 @@ end
: Expr -> Expr
[(1 + 1)]
: Expr
-Let "x" e1 e2
- : expr
-Let "x" e1 e2
- : expr
-Let "x" e1 e2 : list string
- : list string
myAnd1 True True
: Prop
r 2 3
@@ -65,8 +59,6 @@ where
|- Type] (pat, p0, p cannot be used)
fun '{| |} => true
: R -> bool
-b = a
- : Prop
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
The command has indeed failed with message:
@@ -85,18 +77,18 @@ fun x : nat => [x]
: nat -> nat
∀ x : nat, x = x
: Prop
-File "stdin", line 226, characters 0-160:
+File "stdin", line 184, characters 0-160:
Warning: Notation "∀ _ .. _ , _" was already defined with a different format
in scope type_scope. [notation-incompatible-format,parsing]
∀x : nat,x = x
: Prop
-File "stdin", line 239, characters 0-60:
+File "stdin", line 197, characters 0-60:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing]
-File "stdin", line 243, characters 0-64:
+File "stdin", line 201, characters 0-64:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing]
-File "stdin", line 248, characters 0-62:
+File "stdin", line 206, characters 0-62:
Warning: Lonely notation "_ %%%% _" was already defined with a different
format. [notation-incompatible-format,parsing]
3 %% 4
@@ -105,10 +97,10 @@ format. [notation-incompatible-format,parsing]
: nat
3 %% 4
: nat
-File "stdin", line 276, characters 0-61:
+File "stdin", line 234, characters 0-61:
Warning: The format modifier is irrelevant for only parsing rules.
[irrelevant-format-only-parsing,parsing]
-File "stdin", line 280, characters 0-63:
+File "stdin", line 238, characters 0-63:
Warning: The only parsing modifier has no effect in Reserved Notation.
[irrelevant-reserved-notation-only-parsing,parsing]
fun x : nat => U (S x)
@@ -119,7 +111,7 @@ fun x : nat => V x
: forall x : nat, nat * (?T -> ?T)
where
?T : [x : nat x0 : ?T |- Type] (x0 cannot be used)
-File "stdin", line 297, characters 0-30:
+File "stdin", line 255, characters 0-30:
Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
0 :=: 0
: Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ce488fe18d..ebad12af88 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -79,35 +79,7 @@ Check [1 + 1].
End C.
-(* An example of interaction between coercion and notations from
- Robbert Krebbers. *)
-
-Require Import String.
-
-Module D.
-
-Inductive expr :=
- | Var : string -> expr
- | Lam : string -> expr -> expr
- | App : expr -> expr -> expr.
-
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-
-Parameter e1 e2 : expr.
-
-Check (Let "x" e1 e2).
-
-Coercion App : expr >-> Funclass.
-
-Check (Let "x" e1 e2).
-
-Axiom free_vars :> expr -> list string.
-
-Check (Let "x" e1 e2) : list string.
-
-End D.
-
-(* Fixing bugs reported by G. Gonthier in #9207 *)
+(* Fixing overparenthesizing reported by G. Gonthier in #9207 (PR #9214, in 8.10)*)
Module I.
@@ -152,20 +124,6 @@ Check fun '{|n:=x|} => true.
End EmptyRecordSyntax.
-Module L.
-
-(* Testing regression #11053 *)
-
-Section Test.
-Variables (A B : Type) (a : A) (b : B).
-Variable c : A -> B.
-Coercion c : A >-> B.
-Notation COERCION := (c).
-Check b = a.
-End Test.
-
-End L.
-
Module M.
(* Accept boxes around the end variables of a recursive notation (if equal boxes) *)
diff --git a/test-suite/output/NotationsCoercions.out b/test-suite/output/NotationsCoercions.out
new file mode 100644
index 0000000000..56145e5fa5
--- /dev/null
+++ b/test-suite/output/NotationsCoercions.out
@@ -0,0 +1,22 @@
+Let "x" e1 e2
+ : expr
+Let "x" e1 e2
+ : expr
+Let "x" e1 e2 : list string
+ : list string
+b = a
+ : Prop
+foo
+ : (_ BitVec 32)
+#[ r ] 0
+ : nat
+##[ r ]
+ : nat
+##[ r ]
+ : nat
+#[ r ] 0
+ : nat
+##[ r ]
+ : nat
+##[ r ]
+ : nat
diff --git a/test-suite/output/NotationsCoercions.v b/test-suite/output/NotationsCoercions.v
new file mode 100644
index 0000000000..0524bed98c
--- /dev/null
+++ b/test-suite/output/NotationsCoercions.v
@@ -0,0 +1,77 @@
+(* Tests about skipping a coercion vs using a notation involving a coercion *)
+
+Require Import String.
+
+(* Skipping a coercion vs using a notation for the application of the
+ coercion (from Robbert Krebbers, see PR #8890) *)
+
+Module A.
+
+Inductive expr :=
+ | Var : string -> expr
+ | Lam : string -> expr -> expr
+ | App : expr -> expr -> expr.
+
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Parameter e1 e2 : expr.
+Check (Let "x" e1 e2). (* always printed the same *)
+Coercion App : expr >-> Funclass.
+Check (Let "x" e1 e2). (* printed the same from #8890, in 8.10 *)
+Axiom free_vars :> expr -> list string.
+Check (Let "x" e1 e2) : list string. (* printed the same from #11172, in 8.12 *)
+
+End A.
+
+(* Skipping a coercion vs using a notation for the coercion itself
+ (regression #11053 in 8.10 after PR #8890, addressed by PR #11090) *)
+
+Module B.
+
+Section Test.
+Variables (A B : Type) (a : A) (b : B).
+Variable c : A -> B.
+Coercion c : A >-> B.
+Notation COERCION := (c).
+Check b = a. (* printed the same except in 8.10 *)
+End Test.
+
+End B.
+
+Module C.
+
+Record word := { rep: Type }.
+Coercion rep : word >-> Sortclass.
+Axiom myword: word.
+Axiom foo: myword.
+Notation "'(_' 'BitVec' '32)'" := (rep myword).
+Check foo. (* printed with Bitvec from #8890 in 8.10 and 8.11, regression due to #11172 in 8.12 *)
+
+End C.
+
+(* Examples involving coercions to funclass *)
+
+Module D.
+
+Record R := { f :> nat -> nat }.
+Axiom r : R.
+Notation "#[ x ]" := (f x).
+Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *)
+Notation "##[ x ]" := (f x 0).
+Check ##[ r ]. (* printed the same from 8.10 *)
+Check #[ r ] 0. (* printed ##[ r ] from 8.10 *)
+
+End D.
+
+(* Same examples with a parameter *)
+
+Module E.
+
+Record R A := { f :> A -> A }.
+Axiom r : R nat.
+Notation "#[ x ]" := (f nat x).
+Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *)
+Notation "##[ x ]" := (f nat x 0).
+Check ##[ r ]. (* printed the same from 8.10 *)
+Check #[ r ] 0. (* printed ##[ r ] from 8.10 *)
+
+End E.
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 9e850ff1c7..f8f2193e03 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -257,9 +257,10 @@ let context ~poly l =
let sigma = Evd.from_env env in
let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
(* Note, we must use the normalized evar from now on! *)
- let sigma = Evd.minimize_universes sigma in
let ce t = Pretyping.check_evars env sigma t in
let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in
+ let sigma, ctx = Evarutil.finalize ~abort_on_undefined_evars:false
+ sigma (fun nf -> List.map (RelDecl.map_constr_het nf) ctx) in
(* reorder, evar-normalize and add implicit status *)
let ctx = List.rev_map (fun d ->
let {binder_name=name}, b, t = RelDecl.to_tuple d in
@@ -267,8 +268,6 @@ let context ~poly l =
| Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.")
| Name id -> id
in
- let b = Option.map (EConstr.to_constr sigma) b in
- let t = EConstr.to_constr sigma t in
let impl = let open Glob_term in
let search x = match x.CAst.v with
| Some (Name id',max) when Id.equal name id' ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:39:26 +0000