diff options
| -rw-r--r-- | parsing/pcoq.ml4 | 5 | ||||
| -rw-r--r-- | pretyping/termops.ml | 9 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 7 | ||||
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 15 |
6 files changed, 39 insertions, 5 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index cab5c1a5d..1e5b21ec4 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -735,7 +735,10 @@ let is_binder_level from e = let rec symbol_of_production assoc from forpat typ = if is_binder_level from typ then - Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200") + if forpat then + Gramext.Snterml (Gram.Entry.obj Constr.pattern,"200") + else + Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200") else if is_self from typ then Gramext.Sself else diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 56e4f6ecc..a49f27ac5 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -1074,6 +1074,15 @@ let assums_of_rel_context sign = | None -> (na, t)::l) sign ~init:[] +let fold_map_rel_context f env sign = + let rec aux env acc = function + | d::sign -> + aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign + | [] -> + acc + in + aux env [] (List.rev sign) + let map_rel_context_with_binders f sign = let rec aux k = function | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 194fa7132..efa31b124 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -267,6 +267,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env val assums_of_rel_context : rel_context -> (name * constr) list val lift_rel_context : int -> rel_context -> rel_context val substl_rel_context : constr list -> rel_context -> rel_context +val fold_map_rel_context : + (env -> constr -> constr) -> env -> rel_context -> rel_context val map_rel_context_with_binders : (int -> constr -> constr) -> rel_context -> rel_context val fold_named_context_both_sides : diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index d3b368952..84ff2608a 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -36,3 +36,10 @@ Section A. Global Notation "'Z'" := O (at level 9). End A. Notation "$ x" := (id x) (at level 30). Check ($ 5). + +(* Check regression of bug #2087 *) + +Notation "'exists' x , P" := (x, P) + (at level 200, x ident, right associativity, only parsing). + +Definition foo P := let '(exists x, Q) := P in x = Q :> nat. diff --git a/toplevel/command.ml b/toplevel/command.ml index 50c78d0ed..70087ecbf 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1132,9 +1132,9 @@ let look_for_mutual_statements thms = let n = List.length thms in let inds = List.map (fun (id,(t,_) as x) -> let (hyps,ccl) = decompose_prod_assum t in - let whnf_hyp_hds = map_rel_context_with_binders - (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c))) - hyps in + let whnf_hyp_hds = fold_map_rel_context + (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) + (Global.env()) hyps in let ind_hyps = List.flatten (list_map_i (fun i (_,b,t) -> match kind_of_term t with diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7f869c166..a043c404b 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -112,6 +112,19 @@ let dotted_location (b,e) = else (String.make (e-b-1) '.', " ") +let blanching_string s i n = + let s = String.sub s i n in + for i = 0 to String.length s - 1 do + let n = Char.code s.[i] in + (* Heuristic: assume utf-8 chars are printed using a single + fixed-size char and therefore contract all utf-8 code into one + space and trailing null chars; in any case, preserve tabulation so + that its effective interpretation in terms of spacing is preserved *) + if 0xC0 > n && n >= 0x80 then s.[i] <- '\000' + else if s.[i] <> '\t' then s.[i] <- ' ' + done; s + + let print_highlight_location ib loc = let (bp,ep) = unloc loc in let bp = bp - ib.start @@ -120,7 +133,7 @@ let print_highlight_location ib loc = match get_bols_of_loc ib (bp,ep) with | ([],(bl,el)) -> (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++ - str"> " ++ str(String.make (bp-bl) ' ') ++ + str"> " ++ str(blanching_string ib.str bl (bp-bl)) ++ str(String.make (ep-bp) '^')) | ((b1,e1)::ml,(bn,en)) -> let (d1,s1) = dotted_location (b1,bp) in |