From 0f1b5603d1922718f36545f201212fc2796f41a4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 24 Sep 2016 20:36:59 +0200 Subject: [notation] Allow to retrieve defined notations. The ML side lacks a method to query Coq for notations with defined parsing/printing rules. This commit adds a method `get_defined_notations` to that purpose. This is very useful for instance in plugins like SerAPI. In the medium-term, the `Notation` interface may benefit from a bit of refactoring to allow programmatic access and manipulation of notations. --- interp/notation.ml | 3 +++ interp/notation.mli | 3 +++ 2 files changed, 6 insertions(+) diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d4..547c72e107 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1011,6 +1011,9 @@ let find_notation_parsing_rules ntn = try pi3 (String.Map.find ntn !notation_rules) with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn) +let get_defined_notations () = + String.Set.elements @@ String.Map.domain !notation_rules + let add_notation_extra_printing_rule ntn k v = try notation_rules := diff --git a/interp/notation.mli b/interp/notation.mli index b47e1975e3..2e92a00a8c 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -203,6 +203,9 @@ val find_notation_extra_printing_rules : notation -> extra_unparsing_rules val find_notation_parsing_rules : notation -> notation_grammar val add_notation_extra_printing_rule : notation -> string -> string -> unit +(** Returns notations with defined parsing/printing rules *) +val get_defined_notations : unit -> notation list + (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3 From 1a3fc19d1160cb3896e62a16c8e68c97880c748b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 14:00:34 -0400 Subject: Move vector/list compat notations to their relevant files Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files. --- test-suite/bugs/closed/4733.v | 8 +++--- test-suite/bugs/closed/4785.v | 2 +- test-suite/bugs/closed/4785_compat_85.v | 46 +++++++++++++++++++++++++++++++++ test-suite/bugs/opened/4803.v | 20 +++++++++++--- test-suite/success/Notations.v | 7 ++++- theories/Compat/Coq84.v | 6 ----- theories/Compat/Coq85.v | 18 ------------- theories/Lists/List.v | 1 + theories/Vectors/VectorDef.v | 5 ++-- 9 files changed, 78 insertions(+), 35 deletions(-) create mode 100644 test-suite/bugs/closed/4785_compat_85.v diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v index ac0653492a..a6ebda61cf 100644 --- a/test-suite/bugs/closed/4733.v +++ b/test-suite/bugs/closed/4733.v @@ -25,16 +25,16 @@ Check [ _ ]%list : list _. Check [ _ ]%vector : Vector.t _ _. Check [ _ ; _ ]%list : list _. Check [ _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. -(* Now these all work, but not so in 8.4. If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *) +(* Now these all work, but not so in 8.4. If we get the ability to remove notations, this section can also just be removed. *) Check [ ]%mylist : mylist _. Check [ ]%list : list _. Check []%vector : Vector.t _ _. diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index 14af2d91df..c3c97d3f59 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -21,7 +21,7 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil : mylist_scope. +Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v new file mode 100644 index 0000000000..9d65840acd --- /dev/null +++ b/test-suite/bugs/closed/4785_compat_85.v @@ -0,0 +1,46 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *) +Require Coq.Lists.List Coq.Vectors.Vector. +Require Coq.Compat.Coq85. + +Module A. +Import Coq.Lists.List Coq.Vectors.Vector. +Import ListNotations. +Check [ ]%list : list _. +Import VectorNotations ListNotations. +Delimit Scope vector_scope with vector. +Check [ ]%vector : Vector.t _ _. +Check []%vector : Vector.t _ _. +Check [ ]%list : list _. +Fail Check []%list : list _. + +Goal True. + idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) +Abort. + +Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Arguments mynil {_}, _. +Arguments mycons {_} _ _. +Notation " [] " := mynil (compat "8.5") : mylist_scope. +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x nil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. + +Import Coq.Compat.Coq85. +Locate Module VectorNotations. +Import VectorDef.VectorNotations. + +Check []%vector : Vector.t _ _. +Check []%mylist : mylist _. +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +End A. + +Module B. +Import Coq.Compat.Coq85. + +Goal True. + idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) +Abort. +End B. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v index 3ca5c095f5..4530548b8f 100644 --- a/test-suite/bugs/opened/4803.v +++ b/test-suite/bugs/opened/4803.v @@ -25,10 +25,24 @@ Check [ _ ]%list : list _. Check [ _ ]%vector : Vector.t _ _. Check [ _ ; _ ]%list : list _. Check [ _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *) +Check [ _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. + +(** Now check that we can add and then remove notations from the parser *) +(* We should be able to stick some vernacular here to remove [] from the parser *) +Fail Remove Notation "[]". +Goal True. + (* This should not be a syntax error; before moving this file to closed, uncomment this line. *) + (* idtac; []. *) + constructor. +Qed. + +Check { _ : _ & _ }. +Reserved Infix "&" (at level 0). +Fail Remove Infix "&". +(* Check { _ : _ & _ }. *) diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 2f7c62972a..30abd961b1 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -58,7 +58,7 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end). (* Check multi-tokens recursive notations *) -Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). +Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). Check [ 0 ]. Check [ 0 # ; 1 ]. @@ -110,3 +110,8 @@ Goal True -> True. intros H. exact H. Qed. (* Check absence of collision on ".." in nested notations with ".." *) Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). + +(* Check that vector notations do not break Ltac [] (bugs #4785, #4733) *) +Require Import Coq.Vectors.VectorDef. +Import VectorNotations. +Goal True. idtac; []. (* important for test: no space here *) constructor. Qed. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 5eecdc64cc..a3e23f91c9 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -74,12 +74,6 @@ Coercion sig_of_sigT : sigT >-> sig. Coercion sigT2_of_sig2 : sig2 >-> sigT2. Coercion sig2_of_sigT2 : sigT2 >-> sig2. -(** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5. This is necessary. These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *) -Require Coq.Lists.List. -Require Coq.Vectors.VectorDef. -Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) : list_scope. -Notation "[ x ; .. ; y ]" := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. - (** In 8.4, the statement of admitted lemmas did not depend on the section variables. *) Unset Keep Admitted Variables. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 54aeeaa114..490e95c918 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -22,21 +22,3 @@ Global Unset Structural Injection. Global Unset Shrink Abstract. Global Unset Shrink Obligations. Global Set Refolding Reduction. - -(** In Coq 8.5, [] meant Vector, and [ ] meant list. Restore this - behavior, to allow user-defined [] to not override vector - notations. See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *) - -Require Coq.Lists.List. -Require Coq.Vectors.VectorDef. -Module Export Coq. -Module Export Vectors. -Module VectorDef. -Export Coq.Vectors.VectorDef. -Module VectorNotations. -Export Coq.Vectors.VectorDef.VectorNotations. -Notation "[]" := (VectorDef.nil _) : vector_scope. -End VectorNotations. -End VectorDef. -End Vectors. -End Coq. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index fc94d7e254..bf21ffb47b 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -27,6 +27,7 @@ Module ListNotations. Notation "[ ]" := nil (format "[ ]") : list_scope. Notation "[ x ]" := (cons x nil) : list_scope. Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope. End ListNotations. Import ListNotations. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index f49b340758..1f8b76cb62 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -295,11 +295,12 @@ End VECTORLIST. Module VectorNotations. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. +Notation "[]" := [] (compat "8.5") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) : vector_scope. Notation "[ x ]" := (x :: []) : vector_scope. -Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope -. +Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope. +Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope. Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. Open Scope vector_scope. End VectorNotations. -- cgit v1.2.3 From e1f25889f88e078dac0f3b454eb16a470dd5f9ae Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 25 Jun 2016 18:59:39 +0200 Subject: [pp] Remove duplicate color logger. We use the same printing path for color and mono terminal output, thus removing the duplicate printers which avoids problems as they don't have to be kept in sync anymore. We tag unconditionally but set the `pp_tag` tagger properly. This removes IO from `Ppstyle` with IMO is the right thing to do. Test suite passes. --- lib/feedback.ml | 104 ++++++++++++++++++++++++++++++++++++++++------------- lib/feedback.mli | 7 ++-- lib/pp.ml | 6 ++-- lib/pp.mli | 6 ++-- lib/ppstyle.ml | 69 ----------------------------------- lib/ppstyle.mli | 9 +---- toplevel/coqtop.ml | 6 ++-- 7 files changed, 90 insertions(+), 117 deletions(-) diff --git a/lib/feedback.ml b/lib/feedback.ml index dd1ca2af36..44b3ee35d7 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -52,8 +52,7 @@ open Pp_control type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit -let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) -let msgnl strm = msgnl_with !std_ft strm +let msgnl_with ?pp_tag fmt strm = msg_with ?pp_tag fmt (strm ++ fnl ()) (* XXX: This is really painful! *) module Emacs = struct @@ -75,45 +74,100 @@ end open Emacs -let dbg_str = str "Debug:" ++ spc () +let dbg_str = tag Ppstyle.(Tag.inj debug_tag tag) (str "Debug:") ++ spc () let info_str = mt () -let warn_str = str "Warning:" ++ spc () -let err_str = str "Error:" ++ spc () +let warn_str = tag Ppstyle.(Tag.inj warning_tag tag) (str "Warning:") ++ spc () +let err_str = tag Ppstyle.(Tag.inj error_tag tag) (str "Error:" ) ++ spc () let make_body quoter info ?loc s = let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in quoter (hov 0 (loc ++ info ++ s)) (* Generic logger *) -let gen_logger dbg err ?loc level msg = match level with - | Debug -> msgnl (make_body dbg dbg_str ?loc msg) - | Info -> msgnl (make_body dbg info_str ?loc msg) - (* XXX: What to do with loc here? *) - | Notice -> msgnl msg +let gen_logger dbg err ?pp_tag ?loc level msg = match level with + | Debug -> msgnl_with ?pp_tag !std_ft (make_body dbg dbg_str ?loc msg) + | Info -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg) + | Notice -> msgnl_with ?pp_tag !std_ft msg | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_str ?loc msg)) () - | Error -> msgnl_with !err_ft (make_body err err_str ?loc msg) + msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) () + | Error -> msgnl_with ?pp_tag !err_ft (make_body err err_str ?loc msg) -(** Standard loggers *) -let std_logger = gen_logger (fun x -> x) (fun x -> x) +(* We provide a generic clear_log_backend callback for backends + wanting to do clenaup after the print. +*) +let std_logger_tag = ref None +let std_logger_cleanup = ref (fun () -> ()) -(* Color logger *) -let color_terminal_logger ?loc level strm = - let msg = Ppstyle.color_msg in - match level with - | Debug -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm - | Info -> msg ?loc !std_ft strm - | Notice -> msg ?loc !std_ft strm - | Warning -> Flags.if_warn (fun () -> - msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) () - | Error -> msg ?loc ~header:("Error", Ppstyle.error_tag) !err_ft strm +let std_logger ?loc level msg = + gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg; + !std_logger_cleanup () (* Rules for emacs: - Debug/info: emacs_quote_info - Warning/Error: emacs_quote_err - Notice: unquoted + + Note the inconsistency. *) -let emacs_logger = gen_logger emacs_quote_info emacs_quote_err +let emacs_logger = gen_logger emacs_quote_info emacs_quote_err ?pp_tag:None + +(** Color logging. Moved from pp_style, it may need some more refactoring *) + +(** Not thread-safe. We should put a lock somewhere if we print from + different threads. Do we? *) +let make_style_stack () = + (** Default tag is to reset everything *) + let empty = Terminal.make () in + let default_tag = Terminal.({ + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; + }) + in + let style_stack = ref [] in + let peek () = match !style_stack with + | [] -> default_tag (** Anomalous case, but for robustness *) + | st :: _ -> st + in + let push tag = + let style = match Ppstyle.get_style tag with + | None -> empty + | Some st -> st + in + (** Use the merging of the latest tag and the one being currently pushed. + This may be useful if for instance the latest tag changes the background and + the current one the foreground, so that the two effects are additioned. *) + let style = Terminal.merge (peek ()) style in + style_stack := style :: !style_stack; + Terminal.eval style + in + let pop _ = match !style_stack with + | [] -> (** Something went wrong, we fallback *) + Terminal.eval default_tag + | _ :: rem -> style_stack := rem; + Terminal.eval (peek ()) + in + let clear () = style_stack := [] in + push, pop, clear + +let init_color_output () = + let open Pp_control in + let push_tag, pop_tag, clear_tag = make_style_stack () in + std_logger_cleanup := clear_tag; + std_logger_tag := Some Ppstyle.pp_tag; + let tag_handler = { + Format.mark_open_tag = push_tag; + Format.mark_close_tag = pop_tag; + Format.print_open_tag = ignore; + Format.print_close_tag = ignore; + } in + Format.pp_set_mark_tags !std_ft true; + Format.pp_set_mark_tags !err_ft true; + Format.pp_set_formatter_tag_functions !std_ft tag_handler; + Format.pp_set_formatter_tag_functions !err_ft tag_handler let logger = ref std_logger let set_logger l = logger := l diff --git a/lib/feedback.mli b/lib/feedback.mli index 48b1c19a67..5160bd5bc1 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -72,11 +72,8 @@ val set_logger : logger -> unit (** [std_logger] standard logger to [stdout/stderr] *) val std_logger : logger -val color_terminal_logger : logger -(* This logger will apply the proper {!Pp_style} tags, and in - particular use the formatters {!Pp_control.std_ft} and - {!Pp_control.err_ft} to display those messages. Be careful this is - not compatible with the Emacs mode! *) +(** [init_color_output ()] Enable color in the std_logger *) +val init_color_output : unit -> unit (** [feedback_logger] will produce feedback messages instead IO events *) val feedback_logger : logger diff --git a/lib/pp.ml b/lib/pp.ml index 7f4bc149dc..6eaad6fa63 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -356,8 +356,8 @@ let pp_with ?pp_tag ft strm = pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm)) (* pretty printing functions WITH FLUSH *) -let msg_with ft strm = - pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) +let msg_with ?pp_tag ft strm = + pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch @@ -365,7 +365,7 @@ let msg_with ft strm = (** Output to a string formatter *) let string_of_ppcmds c = - Format.fprintf Format.str_formatter "@[%a@]" msg_with c; + Format.fprintf Format.str_formatter "@[%a@]" (msg_with ?pp_tag:None) c; Format.flush_str_formatter () (* Copy paste from Util *) diff --git a/lib/pp.mli b/lib/pp.mli index 3bd560812e..e6542bae5d 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -173,8 +173,8 @@ val pr_loc : Loc.t -> std_ppcmds (** FIXME: These ignore the logging settings and call [Format] directly *) type tag_handler = Tag.t -> Format.tag -(** [msg_with fmt pp] Print [pp] to [fmt] and flush [fmt] *) -val msg_with : Format.formatter -> std_ppcmds -> unit +(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt] *) +val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit -(** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) +(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index ecfaa822c7..aa47c51671 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -56,41 +56,6 @@ let default = Terminal.({ let empty = Terminal.make () -let make_style_stack style_tags = - (** Not thread-safe. We should put a lock somewhere if we print from - different threads. Do we? *) - let style_stack = ref [] in - let peek () = match !style_stack with - | [] -> default (** Anomalous case, but for robustness *) - | st :: _ -> st - in - let push tag = - let style = - try - begin match String.Map.find tag style_tags with - | None -> empty - | Some st -> st - end - with Not_found -> empty - in - (** Use the merging of the latest tag and the one being currently pushed. - This may be useful if for instance the latest tag changes the background and - the current one the foreground, so that the two effects are additioned. *) - let style = Terminal.merge (peek ()) style in - let () = style_stack := style :: !style_stack in - Terminal.eval style - in - let pop _ = match !style_stack with - | [] -> - (** Something went wrong, we fallback *) - Terminal.eval default - | _ :: rem -> - let () = style_stack := rem in - Terminal.eval (peek ()) - in - let clear () = style_stack := [] in - push, pop, clear - let error_tag = let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in make ~style ["message"; "error"] @@ -106,37 +71,3 @@ let debug_tag = let pp_tag t = match Pp.Tag.prj t tag with | None -> "" | Some key -> key - -let clear_tag_fn = ref (fun () -> ()) - -let init_color_output () = - let push_tag, pop_tag, clear_tag = make_style_stack !tags in - clear_tag_fn := clear_tag; - let tag_handler = { - Format.mark_open_tag = push_tag; - Format.mark_close_tag = pop_tag; - Format.print_open_tag = ignore; - Format.print_close_tag = ignore; - } in - let open Pp_control in - Format.pp_set_mark_tags !std_ft true; - Format.pp_set_mark_tags !err_ft true; - Format.pp_set_formatter_tag_functions !std_ft tag_handler; - Format.pp_set_formatter_tag_functions !err_ft tag_handler - -let color_msg ?loc ?header ft strm = - let pptag = tag in - let open Pp in - let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in - let strm = match header with - | None -> hov 0 (ploc ++ strm) - | Some (h, t) -> - let tag = Pp.Tag.inj t pptag in - let h = Pp.tag tag (str h ++ str ":") in - hov 0 (ploc ++ h ++ spc () ++ strm) - in - pp_with ~pp_tag ft strm; - Format.pp_print_newline ft (); - Format.pp_print_flush ft (); - (** In case something went wrong, we reset the stack *) - !clear_tag_fn () diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli index b07fcd5d4c..d9fd757656 100644 --- a/lib/ppstyle.mli +++ b/lib/ppstyle.mli @@ -44,14 +44,7 @@ val parse_config : string -> unit val dump : unit -> (t * Terminal.style option) list (** Recover the list of known tags together with their current style. *) -(** {5 Setting color output} *) - -val init_color_output : unit -> unit - -val color_msg : ?loc:Loc.t -> ?header:string * Format.tag -> - Format.formatter -> Pp.std_ppcmds -> unit -(** {!color_msg ?header fmt pp} will format according to the tags - defined in this file *) +(** {5 Color output} *) val pp_tag : Pp.tag_handler (** Returns the name of a style tag that is understandable by the formatters diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 47d433d790..65ffa6f84d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -61,8 +61,7 @@ let init_color () = match colors with | None -> (** Default colors *) - Ppstyle.init_color_output (); - Feedback.set_logger Feedback.color_terminal_logger + Feedback.init_color_output () | Some "" -> (** No color output *) () @@ -70,8 +69,7 @@ let init_color () = (** Overwrite all colors *) Ppstyle.clear_styles (); Ppstyle.parse_config s; - Ppstyle.init_color_output (); - Feedback.set_logger Feedback.color_terminal_logger + Feedback.init_color_output () end let toploop_init = ref begin fun x -> -- cgit v1.2.3 From fd39a2e844f93b314c2f0b78510f0573cfa1bef3 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 6 Oct 2016 19:34:28 +0200 Subject: Revert "Make the pretty printer resilient to incomplete nametab (progress on #4363)." This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402. This fixes bug #4874. We fallback to the original error message of v8.4. The fallback printer introduced in this commit only gave unqualified names, which is what this bug reports. --- interp/constrextern.ml | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 68a3cf0f4a..ae9b5bace2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -147,17 +147,8 @@ let extern_evar loc n l = CEvar (loc,n,l) For instance, in the debugger the tables of global references may be inaccurate *) -let safe_shortest_qualid_of_global vars r = - try shortest_qualid_of_global vars r - with Not_found -> - match r with - | VarRef v -> make_qualid DirPath.empty v - | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c)) - | IndRef (i,_) | ConstructRef ((i,_),_) -> - make_qualid DirPath.empty Names.(Label.to_id (mind_label i)) - let default_extern_reference loc vars r = - Qualid (loc,safe_shortest_qualid_of_global vars r) + Qualid (loc,shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference -- cgit v1.2.3 From 2faa03903f63523707503ff7b10acac0f959ed0a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Oct 2016 23:28:12 +0200 Subject: Remove dead code in Environ. --- kernel/environ.ml | 12 ------------ kernel/environ.mli | 8 -------- 2 files changed, 20 deletions(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index 54898320dd..16ddfac64b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -502,18 +502,6 @@ let apply_to_hyp ctxt id f = | None -> raise Hyp_not_found in aux [] ctxt -let apply_to_hyp_and_dependent_on ctxt id f g = - let rec aux sign = - match match_named_context_val sign with - | Some (d, v, sign) -> - if Id.equal (get_id d) id then - push_named_context_val (f d sign) sign - else - let sign = aux sign in - push_named_context_val (g d sign) sign - | None -> raise Hyp_not_found - in aux ctxt - (* To be used in Logic.clear_hyps *) let remove_hyps ids check_context check_value ctxt = let rec remove_hyps ctxt = match match_named_context_val ctxt with diff --git a/kernel/environ.mli b/kernel/environ.mli index 235ba2fd14..6ac00088b3 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -264,14 +264,6 @@ val apply_to_hyp : named_context_val -> variable -> (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> named_context_val -(** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into - [tail::(id,_,_)::head] and - return [(g tail)::(f (id,_,_))::head]. *) -val apply_to_hyp_and_dependent_on : named_context_val -> variable -> - (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> - (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> - named_context_val - val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val -- cgit v1.2.3 From db18609c06b73ac168ad06a0c2073188587f5814 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 13 Oct 2016 09:07:55 +0200 Subject: Completing reverting generalization and cleaning of the return clause inference. Revert "Inference of return clause: giving uniformly priority to "small inversion"." This reverts commit 980b434552d73cb990860f8d659b64686f6dbc87. --- pretyping/cases.ml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 98d3000885..0ac34b7186 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1925,7 +1925,10 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = * type and 1 assumption for each term not _syntactically_ in an * inductive type. - * Each matched term is independently considered dependent or not. + * Each matched terms are independently considered dependent or not. + + * A type constraint but no annotation case: we try to specialize the + * tycon to make the predicate if it is not closed. *) let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = @@ -1935,14 +1938,14 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = | None, Some t when not (noccur_with_meta 0 max_int t) -> (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) - (* First strategy: we build an "inversion" predicate *) - let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in - (* Optional second strategy: we abstract the tycon wrt to the dependencies *) - let p2 = + (* First strategy: we abstract the tycon wrt to the dependencies *) + let p1 = prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in - (match p2 with - | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2] - | None -> [sigma1, pred1]) + (* Second strategy: we build an "inversion" predicate *) + let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in + (match p1 with + | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2] + | None -> [sigma2, pred2]) | None, _ -> (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) @@ -1957,7 +1960,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = in (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in - (* Second strategy: we use the evar or tycon as a non dependent pred *) + (* Second strategy: we directly use the evar as a non dependent pred *) let pred2 = lift (List.length (List.flatten arsign)) t in [sigma1, pred1; sigma, pred2] (* Some type annotation *) -- cgit v1.2.3 From d8e87360b6413d9eb02c2c47441c8f48b816eac3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Oct 2016 19:06:10 +0200 Subject: Using "simple apply" and "simple eapply" in the trace of auto. This is more precise and probably clearer (see e.g. thread "Understanding auto" on coq-club). --- tactics/hints.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index d1343f296e..89ecc6c0b2 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1297,11 +1297,11 @@ let make_db_list dbnames = let pr_hint_elt (c, _, _) = pr_constr c let pr_hint h = match h.obj with - | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c) - | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c) + | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c) + | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c) | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c) | Res_pf_THEN_trivial_fail (c, _) -> - (str"apply " ++ pr_hint_elt c ++ str" ; trivial") + (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> let env = -- cgit v1.2.3 From a40451fbd096703d9a06795c9294d11dfd7a74dd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Oct 2016 19:59:46 +0200 Subject: Fixing English typography for colon. --- tactics/auto.ml | 8 ++++---- tactics/eauto.ml | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tactics/auto.ml b/tactics/auto.ml index 6d1a1ae28f..a6dc64b4e4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -269,10 +269,10 @@ let pr_info_nop = function let pr_dbg_header = function | (Off,_,_) -> mt () - | (Debug,0,_) -> str "(* debug trivial : *)" - | (Debug,_,_) -> str "(* debug auto : *)" - | (Info,0,_) -> str "(* info trivial : *)" - | (Info,_,_) -> str "(* info auto : *)" + | (Debug,0,_) -> str "(* debug trivial: *)" + | (Debug,_,_) -> str "(* debug auto: *)" + | (Info,0,_) -> str "(* info trivial: *)" + | (Info,_,_) -> str "(* info auto: *)" let tclTRY_dbg d tac = let (level, _, _) = d in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 90f80a7377..c6d2448679 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -351,8 +351,8 @@ let pr_info_nop = function let pr_dbg_header = function | Off -> () - | Debug -> Feedback.msg_debug (str "(* debug eauto : *)") - | Info -> Feedback.msg_debug (str "(* info eauto : *)") + | Debug -> Feedback.msg_debug (str "(* debug eauto: *)") + | Info -> Feedback.msg_debug (str "(* info eauto: *)") let pr_info dbg s = if dbg != Info then () -- cgit v1.2.3 From 58d1381316560eadbe859b53780fe8da7723ad31 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Oct 2016 20:03:23 +0200 Subject: Fixing printing of info_auto broken since 0091c528 (2014). --- tactics/auto.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tactics/auto.ml b/tactics/auto.ml index 45da04cf00..65294dadad 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -272,8 +272,8 @@ let tclTRY_dbg d tac = let (level, _, _) = d in let delay f = Proofview.tclUNIT () >>= fun () -> f () in let tac = match level with - | Off -> tac - | Debug | Info -> delay (fun () -> msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac) + | Debug | Off -> tac + | Info -> delay (fun () -> msg_debug (pr_dbg_header d); tac) >>= fun () -> msg_debug (pr_info_trace d); Proofview.tclUNIT () in let after = match level with | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ()) -- cgit v1.2.3 From 7c047370dc9032e3ded3365a45de5b92e7c9033f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Oct 2016 22:12:53 +0200 Subject: Fix bug #5139: Anomalies should not be caught by || / try. There was a catch-all clause in the tclORELSE0 function. We now only catch noncritical exceptions. --- tactics/tacticals.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 87fdcf14d4..66da9ee182 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -322,7 +322,7 @@ module New = struct try Refiner.catch_failerror e; tclUNIT () - with e -> tclZERO e + with e when CErrors.noncritical e -> tclZERO e (* spiwack: I chose to give the Ltac + the same semantics as [Proofview.tclOR], however, for consistency with the or-else -- cgit v1.2.3 From ec878d596f15ad2baa10395fffd3849df5597f78 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 15 Oct 2016 00:24:20 +0200 Subject: One more little bug in the output of "debug auto". Header was missing in last commit. One day, it would be nice to unify the display of "debug auto" and "debug eauto"... --- tactics/auto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/auto.ml b/tactics/auto.ml index 65294dadad..985650e49d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -272,7 +272,7 @@ let tclTRY_dbg d tac = let (level, _, _) = d in let delay f = Proofview.tclUNIT () >>= fun () -> f () in let tac = match level with - | Debug | Off -> tac + | Debug | Off -> delay (fun () -> msg_debug (pr_dbg_header d); tac) | Info -> delay (fun () -> msg_debug (pr_dbg_header d); tac) >>= fun () -> msg_debug (pr_info_trace d); Proofview.tclUNIT () in let after = match level with -- cgit v1.2.3 From e349809cf36289dc73249b2861007cc24e01bfa7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 15 Oct 2016 01:04:02 +0200 Subject: Still a problem with debug auto printing. "msg_debug (mt())" is not identity, so we return back to how it was done in 8.4, contracting a repeated pattern-matching into one. --- tactics/auto.ml | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/tactics/auto.ml b/tactics/auto.ml index 985650e49d..fd25265e96 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -254,31 +254,25 @@ let pr_info_atom (d,pp) = let pr_info_trace = function | (Info,_,{contents=(d,Some pp)::l}) -> - prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l) - | _ -> mt () + msg_debug (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) + | _ -> () let pr_info_nop = function - | (Info,_,_) -> str "idtac." - | _ -> mt () + | (Info,_,_) -> msg_debug (str "idtac.") + | _ -> () let pr_dbg_header = function - | (Off,_,_) -> mt () - | (Debug,0,_) -> str "(* debug trivial : *)" - | (Debug,_,_) -> str "(* debug auto : *)" - | (Info,0,_) -> str "(* info trivial : *)" - | (Info,_,_) -> str "(* info auto : *)" + | (Off,_,_) -> () + | (Debug,0,_) -> msg_debug (str "(* debug trivial : *)") + | (Debug,_,_) -> msg_debug (str "(* debug auto : *)") + | (Info,0,_) -> msg_debug (str "(* info trivial : *)") + | (Info,_,_) -> msg_debug (str "(* info auto : *)") let tclTRY_dbg d tac = - let (level, _, _) = d in let delay f = Proofview.tclUNIT () >>= fun () -> f () in - let tac = match level with - | Debug | Off -> delay (fun () -> msg_debug (pr_dbg_header d); tac) - | Info -> delay (fun () -> msg_debug (pr_dbg_header d); tac) >>= fun () -> msg_debug (pr_info_trace d); Proofview.tclUNIT () - in - let after = match level with - | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ()) - | Off | Debug -> Proofview.tclUNIT () - in + let tac = delay (fun () -> pr_dbg_header d; tac) >>= + fun () -> pr_info_trace d; Proofview.tclUNIT () in + let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in Tacticals.New.tclORELSE0 tac after (**************************************************************************) -- cgit v1.2.3 From c3b9a7bf9fcd162628ce6a2a544652ca096cfe54 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Oct 2016 16:27:37 +0200 Subject: Fix bug #5145: Anomaly: index to an anonymous variable. When printing evar constraints, we ensure that every variable from the rel context has a name. --- engine/evd.ml | 1 + test-suite/bugs/closed/5145.v | 10 ++++++++++ 2 files changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/5145.v diff --git a/engine/evd.ml b/engine/evd.ml index 6ba8a51120..291c089784 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1411,6 +1411,7 @@ let print_env_short env = let pr_evar_constraints pbs = let pr_evconstr (pbty, env, t1, t2) = + let env = Namegen.make_all_name_different env in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ print_constr_env env t1 ++ spc () ++ str (match pbty with diff --git a/test-suite/bugs/closed/5145.v b/test-suite/bugs/closed/5145.v new file mode 100644 index 0000000000..0533d21e0c --- /dev/null +++ b/test-suite/bugs/closed/5145.v @@ -0,0 +1,10 @@ +Class instructions := + { + W : Type; + ldi : nat -> W + }. + +Fail Definition foo := + let y2 := ldi 0 in + let '(CF, _) := (true, 0) in + y2. -- cgit v1.2.3 From 67c713cab69a54f5347c987aa0076aeddd1bceef Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Oct 2016 19:04:29 +0200 Subject: Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching". We simply explicit that the type is actually referring to the return type, not to the type of the argument of the pattern-matching. Note that the heuristic could be enhanced so as to use the same code in both let-style and match-style pattern-matching, but I'm leaving this for another time. --- toplevel/himsg.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6ee695bc24..56b4779555 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -516,7 +516,8 @@ let explain_cant_find_case_type env sigma c = let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in let pe = pr_lconstr_env env sigma c in - str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." + str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++ + pe ++ str "." let explain_occur_check env sigma ev rhs = let rhs = Evarutil.nf_evar sigma rhs in -- cgit v1.2.3 From e5f8038f82c8a444afcfb7333a4c690b005fcff6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Oct 2016 11:58:21 +0200 Subject: Fix bug #5023: JSON extraction doesn't generate "for xxx". --- plugins/extraction/json.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 8874afef33..e43c47d050 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -142,7 +142,8 @@ let rec json_expr env = function ("what", json_str "fix:item"); ("name", json_id fi); ("body", json_function env' ti) - ]) (Array.map2 (fun a b -> a,b) ids' defs))) + ]) (Array.map2 (fun a b -> a,b) ids' defs))); + ("for", json_int i); ] | MLexn s -> json_dict [ ("what", json_str "expr:exception"); -- cgit v1.2.3 From 159b10655172b6f0888f9622be3620c3c33d35b1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Oct 2016 12:17:01 +0200 Subject: Test for bug #4874. --- test-suite/output/qualification.out | 3 +++ test-suite/output/qualification.v | 19 +++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 test-suite/output/qualification.out create mode 100644 test-suite/output/qualification.v diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out new file mode 100644 index 0000000000..3cf3c2d8fb --- /dev/null +++ b/test-suite/output/qualification.out @@ -0,0 +1,3 @@ +File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7: +Error: Signature components for label test do not match: expected type +"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v new file mode 100644 index 0000000000..d39097e2dd --- /dev/null +++ b/test-suite/output/qualification.v @@ -0,0 +1,19 @@ +Module Type T1. + Parameter t : Type. +End T1. + +Module Type T2. + Declare Module M : T1. + Parameter t : Type. + Parameter test : t = M.t. +End T2. + +Module M1 <: T1. + Definition t : Type := bool. +End M1. + +Module M2 <: T2. + Module M := M1. + Definition t : Type := nat. + Lemma test : t = t. Proof. reflexivity. Qed. +End M2. -- cgit v1.2.3 From 502d901fee12f07c31c2ea8b8c1455f74876d986 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 17 Oct 2016 15:55:53 +0200 Subject: Example illustrating non-local inference of the default type of impossible branches (see PR #323). --- test-suite/success/CaseInClause.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v index 599b9566cb..6424fe92dd 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -24,3 +24,6 @@ Theorem foo : forall (n m : nat) (pf : n = m), (* Check redundant clause is removed *) Inductive I : nat * nat -> Type := C : I (0,0). Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end. + +(* An example of non-local inference of the type of an impossible case *) +Check (fun y n (x:Vector.t nat (S n)) => match x with a::_ => a | _ => y end) 2. -- cgit v1.2.3 From 409bc943e8d8a0bc0d35ae63f3530b7324ca975e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Oct 2016 17:24:32 +0200 Subject: Fix previous commit. I've messed up with parts of the compatibility files I had to commit. --- theories/Compat/Coq85.v | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 74b416aae7..4007536442 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -27,21 +27,3 @@ Global Set Refolding Reduction. Global Set Typeclasses Legacy Resolution. Global Set Typeclasses Limit Intros. Global Unset Typeclasses Filtered Unification. - -(** In Coq 8.5, [] meant Vector, and [ ] meant list. Restore this - behavior, to allow user-defined [] to not override vector - notations. See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *) - -Require Coq.Lists.List. -Require Coq.Vectors.VectorDef. -Module Export Coq. -Module Export Vectors. -Module VectorDef. -Export Coq.Vectors.VectorDef. -Module VectorNotations. -Export Coq.Vectors.VectorDef.VectorNotations. -Notation "[]" := (VectorDef.nil _) : vector_scope. -End VectorNotations. -End VectorDef. -End Vectors. -End Coq. -- cgit v1.2.3 From 48b342ed5b9fb514961e10b2684243dc0b4078be Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Oct 2016 17:37:15 +0200 Subject: Fix output test for module qualification. The output was embedding local paths from my machine. --- test-suite/output/qualification.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out index 3cf3c2d8fb..9300c3f546 100644 --- a/test-suite/output/qualification.out +++ b/test-suite/output/qualification.out @@ -1,3 +1,3 @@ -File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7: +File "stdin", line 19, characters 0-7: Error: Signature components for label test do not match: expected type "Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". -- cgit v1.2.3