diff options
45 files changed, 461 insertions, 306 deletions
diff --git a/API/API.mli b/API/API.mli index 3ed008ff5..c5a1743f7 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4801,7 +4801,7 @@ sig | IntroNeedsProduct | DoesNotOccurIn of Constr.t * Names.Id.t | NoSuchHyp of Names.Id.t - exception RefinerError of refiner_error + exception RefinerError of Environ.env * Evd.evar_map * refiner_error val catchable_exception : exn -> bool end diff --git a/configure.ml b/configure.ml index c7d25bfc8..3850f119b 100644 --- a/configure.ml +++ b/configure.ml @@ -178,6 +178,20 @@ let which prog = let program_in_path prog = try let _ = which prog in true with Not_found -> false +(** Choose a command among a list of candidates + (command name, mandatory arguments, arguments for this test). + Chooses the first one whose execution outputs a non-empty (first) line. + Dies with message [msg] if none is found. *) + +let select_command msg candidates = + let rec search = function + | [] -> die msg + | (p, x, y) :: tl -> + if fst (tryrun p (x @ y)) <> "" + then List.fold_left (Printf.sprintf "%s %s") p x + else search tl + in search candidates + (** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it a quoted path to camlpXo via -pp. So we only quote camlpXo on not Windows, and warn on Windows if the path contains spaces *) @@ -853,9 +867,10 @@ let strip = (** * md5sum command *) let md5sum = - if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"] - then "md5 -q" else "md5sum" - + select_command "Don’t know how to compute MD5 checksums…" [ + "md5sum", [], [ "--version" ]; + "md5", ["-q"], [ "-s" ; "''" ]; + ] (** * Documentation : do we have latex, hevea, ... *) diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index ecf7880e2..87a829746 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -11,6 +11,13 @@ CODE=0 if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; then + # skip PRs from before the linter existed + if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; + then + 2>&1 echo "Linting skipped: pull request older than the linter." + exit 0 + fi + # Some problems are too widespread to fix in one commit, but we # can still check that they don't worsen. CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 907f1b1ac..3445b744a 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -199,9 +199,10 @@ let whd_head_evar sigma c = let meta_counter_summary_name = "meta counter" (* Generator of metavariables *) -let new_meta = - let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in - fun () -> incr meta_ctr; !meta_ctr +let meta_ctr, meta_counter_summary_tag = + Summary.ref_tag 0 ~name:meta_counter_summary_name + +let new_meta () = incr meta_ctr; !meta_ctr let mk_new_meta () = EConstr.mkMeta(new_meta()) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 5fd4634d6..9d0b973a7 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -236,7 +236,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> val subterm_source : Evar.t -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located -val meta_counter_summary_name : string +val meta_counter_summary_tag : int Summary.Dyn.tag (** Deprecated *) type type_constraint = types option diff --git a/engine/evd.ml b/engine/evd.ml index 45d2a8b08..e33c851f6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -466,9 +466,8 @@ let add d e i = add_with_name d e i let evar_counter_summary_name = "evar counter" (* Generator of existential names *) -let new_untyped_evar = - let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in - fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr +let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name +let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr let new_evar evd ?name evi = let evk = new_untyped_evar () in diff --git a/engine/evd.mli b/engine/evd.mli index 636bd1be1..b28ce2a62 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -613,7 +613,7 @@ type unsolvability_explanation = SeveralInstancesFound of int (* This stuff is internal and should not be used. Currently a hack in the STM relies on it. *) -val evar_counter_summary_name : string +val evar_counter_summary_tag : int Summary.Dyn.tag (** {5 Deprecated functions} *) val create_evar_defs : evar_map -> evar_map diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bd43d1ffc..58599a14d 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -376,15 +376,8 @@ let init = match file with | None -> init_sid | Some file -> - let dir = Filename.dirname file in - let open Loadpath in let open CUnix in let doc, initial_id, _ = - let doc = get_doc () in - if not (is_in_load_paths (physical_path_of_string dir)) then begin - let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in - let loc_ast = Stm.parse_sentence ~doc init_sid pa in - Stm.add false ~doc ~ontop:init_sid loc_ast - end else doc, init_sid, `NewTip in + get_doc (), init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; set_doc (Stm.finish ~doc); diff --git a/lib/dyn.ml b/lib/dyn.ml index 83e673d2c..64535d35f 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -55,6 +55,8 @@ sig include PreS module Easy : sig + + val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag val make_dyn : string -> ('a -> t) * (t -> 'a) val inj : 'a -> 'a tag -> t val prj : t -> 'a tag -> 'a option @@ -129,8 +131,9 @@ end include Self module Easy = struct + (* now tags are opaque, we can do the trick *) -let make_dyn (s : string) = +let make_dyn_tag (s : string) = (fun (type a) (tag : a tag) -> let infun : (a -> t) = fun x -> Dyn (tag, x) in let outfun : (t -> a) = fun (Dyn (t, x)) -> @@ -138,9 +141,12 @@ let make_dyn (s : string) = | None -> assert false | Some CSig.Refl -> x in - (infun, outfun)) + infun, outfun, tag) (create s) +let make_dyn (s : string) = + let inf, outf, _ = make_dyn_tag s in inf, outf + let inj x tag = Dyn(tag,x) let prj : type a. t -> a tag -> a option = fun (Dyn(tag',x)) tag -> diff --git a/lib/dyn.mli b/lib/dyn.mli index e0e1a9d14..2206394e2 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -53,6 +53,7 @@ val dump : unit -> (int * string) list module Easy : sig (* To create a dynamic type on the fly *) + val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag val make_dyn : string -> ('a -> t) * (t -> 'a) (* For types declared with the [create] function above *) diff --git a/library/global.ml b/library/global.ml index 03d7612a4..ce37dfecf 100644 --- a/library/global.ml +++ b/library/global.ml @@ -20,6 +20,7 @@ module GlobalSafeEnv : sig val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_joined_environment : unit -> bool + val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag end = struct @@ -30,9 +31,9 @@ let join_safe_environment ?except () = let is_joined_environment () = Safe_typing.is_joined_environment !global_env - -let () = - Summary.declare_summary global_env_summary_name + +let global_env_summary_tag = + Summary.declare_summary_tag global_env_summary_name { Summary.freeze_function = (function | `Yes -> join_safe_environment (); !global_env | `No -> !global_env @@ -51,6 +52,8 @@ let set_safe_env e = global_env := e end +let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag + let safe_env = GlobalSafeEnv.safe_env let join_safe_environment ?except () = GlobalSafeEnv.join_safe_environment ?except () diff --git a/library/global.mli b/library/global.mli index c62462f9f..324181e79 100644 --- a/library/global.mli +++ b/library/global.mli @@ -159,4 +159,4 @@ val current_dirpath : unit -> DirPath.t val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a -val global_env_summary_name : string +val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag diff --git a/library/summary.ml b/library/summary.ml index 9f49d1f83..6df17476b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -13,17 +13,22 @@ open Util module Dyn = Dyn.Make () type marshallable = [ `Yes | `No | `Shallow ] + type 'a summary_declaration = { freeze_function : marshallable -> 'a; unfreeze_function : 'a -> unit; init_function : unit -> unit } -let summaries = ref Int.Map.empty +let sum_mod = ref None +let sum_map = ref String.Map.empty let mangle id = id ^ "-SUMMARY" +let unmangle id = String.(sub id 0 (length id - 8)) + +let ml_modules = "ML-MODULES" -let internal_declare_summary hash sumname sdecl = - let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in +let internal_declare_summary fadd sumname sdecl = + let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -32,140 +37,116 @@ let internal_declare_summary hash sumname sdecl = unfreeze_function = dyn_unfreeze; init_function = dyn_init } in - summaries := Int.Map.add hash (sumname, ddecl) !summaries + fadd sumname ddecl; + tag -let all_declared_summaries = ref Int.Set.empty +let declare_ml_modules_summary decl = + let ml_add _ ddecl = sum_mod := Some ddecl in + internal_declare_summary ml_add ml_modules decl -let summary_names = ref [] -let name_of_summary name = - try List.assoc name !summary_names - with Not_found -> "summary name not found" +let declare_ml_modules_summary decl = + ignore(declare_ml_modules_summary decl) -let declare_summary sumname decl = - let hash = String.hash sumname in - let () = if Int.Map.mem hash !summaries then - let (name, _) = Int.Map.find hash !summaries in - anomaly ~label:"Summary.declare_summary" - (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".") +let declare_summary_tag sumname decl = + let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in + let () = if String.Map.mem sumname !sum_map then + anomaly ~label:"Summary.declare_summary" + (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".") in - all_declared_summaries := Int.Set.add hash !all_declared_summaries; - summary_names := (hash, sumname) :: !summary_names; - internal_declare_summary hash sumname decl + internal_declare_summary fadd sumname decl + +let declare_summary sumname decl = + ignore(declare_summary_tag sumname decl) type frozen = { - summaries : (int * Dyn.t) list; + summaries : Dyn.t String.Map.t; (** Ordered list w.r.t. the first component. *) ml_module : Dyn.t option; (** Special handling of the ml_module summary. *) } -let empty_frozen = { summaries = []; ml_module = None; } - -let ml_modules = "ML-MODULES" -let ml_modules_summary = String.hash ml_modules +let empty_frozen = { summaries = String.Map.empty; ml_module = None } let freeze_summaries ~marshallable : frozen = - let fold id (_, decl) accu = - (* to debug missing Lazy.force - if marshallable <> `No then begin - let id, _ = Int.Map.find id !summaries in - prerr_endline ("begin marshalling " ^ id); - ignore(Marshal.to_string (decl.freeze_function marshallable) []); - prerr_endline ("end marshalling " ^ id); - end; - /debug *) - let state = decl.freeze_function marshallable in - if Int.equal id ml_modules_summary then { accu with ml_module = Some state } - else { accu with summaries = (id, state) :: accu.summaries } + let smap decl = decl.freeze_function marshallable in + { summaries = String.Map.map smap !sum_map; + ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod; + } + +let unfreeze_single name state = + let decl = + try String.Map.find name !sum_map + with + | Not_found -> + CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name) in - Int.Map.fold_right fold !summaries empty_frozen - -let unfreeze_summaries fs = + try decl.unfreeze_function state + with e when CErrors.noncritical e -> + let e = CErrors.push e in + Feedback.msg_warning + Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); + iraise e + +let unfreeze_summaries ?(partial=false) { summaries; ml_module } = (* The unfreezing of [ml_modules_summary] has to be anticipated since it - * may modify the content of [summaries] ny loading new ML modules *) - let (_, decl) = - try Int.Map.find ml_modules_summary !summaries - with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") - in - let () = match fs.ml_module with + * may modify the content of [summaries] by loading new ML modules *) + begin match !sum_mod with | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") - | Some state -> decl.unfreeze_function state - in - let fold id (_, decl) states = - if Int.equal id ml_modules_summary then states - else match states with - | [] -> - let () = decl.init_function () in - [] - | (nid, state) :: rstates -> - if Int.equal id nid then - let () = decl.unfreeze_function state in rstates - else - let () = decl.init_function () in states + | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module + end; + (** We must be independent on the order of the map! *) + let ufz name decl = + try decl.unfreeze_function String.Map.(find name summaries) + with Not_found -> + if not partial then begin + Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); + decl.init_function () + end; in - let fold id decl state = - try fold id decl state - with e when CErrors.noncritical e -> - let e = CErrors.push e in - Feedback.msg_error - Pp.(seq [str "Error unfreezing summary %s\n%s\n%!"; - str (name_of_summary id); - CErrors.iprint e]); - iraise e - in - (** We rely on the order of the frozen list, and the order of folding *) - ignore (Int.Map.fold_left fold !summaries fs.summaries) + (* String.Map.iter unfreeze_single !sum_map *) + String.Map.iter ufz !sum_map let init_summaries () = - Int.Map.iter (fun _ (_, decl) -> decl.init_function ()) !summaries + String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map (** For global tables registered statically before the end of coqtop launch, the following empty [init_function] could be used. *) let nop () = () -(** Selective freeze *) +(** Summary projection *) +let project_from_summary { summaries } tag = + let id = unmangle (Dyn.repr tag) in + let state = String.Map.find id summaries in + Option.get (Dyn.Easy.prj state tag) + +let modify_summary st tag v = + let id = unmangle (Dyn.repr tag) in + let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in + {st with summaries} -type frozen_bits = (int * Dyn.t) list +let remove_from_summary st tag = + let id = unmangle (Dyn.repr tag) in + let summaries = String.Map.remove id st.summaries in + {st with summaries} + +(** Selective freeze *) -let ids_of_string_list complement ids = - if not complement then List.map String.hash ids - else - let fold accu id = - let id = String.hash id in - Int.Set.remove id accu - in - let ids = List.fold_left fold !all_declared_summaries ids in - Int.Set.elements ids +type frozen_bits = Dyn.t String.Map.t let freeze_summary ~marshallable ?(complement=false) ids = - let ids = ids_of_string_list complement ids in - List.map (fun id -> - let (_, summary) = Int.Map.find id !summaries in - id, summary.freeze_function marshallable) - ids - -let unfreeze_summary datas = - List.iter - (fun (id, data) -> - let (name, summary) = Int.Map.find id !summaries in - try summary.unfreeze_function data - with e -> - let e = CErrors.push e in - prerr_endline ("Exception unfreezing " ^ name); - iraise e) - datas + let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in + String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map + +let unfreeze_summary = String.Map.iter unfreeze_single let surgery_summary { summaries; ml_module } bits = - let summaries = List.map (fun (id, _ as orig) -> - try id, List.assoc id bits - with Not_found -> orig) - summaries in + let summaries = + String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in { summaries; ml_module } let project_summary { summaries; ml_module } ?(complement=false) ids = - let ids = ids_of_string_list complement ids in - List.filter (fun (id, _) -> List.mem id ids) summaries + String.Map.filter (fun name _ -> complement <> List.(mem name ids)) summaries let pointer_equal l1 l2 = let ptr_equal d1 d2 = @@ -174,19 +155,22 @@ let pointer_equal l1 l2 = match Dyn.eq t1 t2 with | None -> false | Some Refl -> x1 == x2 - in + in + let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in CList.for_all2eq (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 (** All-in-one reference declaration + registration *) -let ref ?(freeze=fun _ r -> r) ~name x = +let ref_tag ?(freeze=fun _ r -> r) ~name x = let r = ref x in - declare_summary name + let tag = declare_summary_tag name { freeze_function = (fun b -> freeze b !r); unfreeze_function = ((:=) r); - init_function = (fun () -> r := x) }; - r + init_function = (fun () -> r := x) } in + r, tag + +let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x module Local = struct @@ -198,8 +182,7 @@ let (!) r = let key, name = !r in try CEphemeron.get key with CEphemeron.InvalidKey -> - let _, { init_function } = - Int.Map.find (String.hash (mangle name)) !summaries in + let { init_function } = String.Map.find name !sum_map in init_function (); CEphemeron.get (fst !r) diff --git a/library/summary.mli b/library/summary.mli index d093d95f2..09447199e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -36,6 +36,12 @@ type 'a summary_declaration = { val declare_summary : string -> 'a summary_declaration -> unit +(** We provide safe projection from the summary to the types stored in + it.*) +module Dyn : Dyn.S + +val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag + (** All-in-one reference declaration + summary registration. It behaves just as OCaml's standard [ref] function, except that a [declare_summary] is done, with [name] as string. @@ -43,6 +49,7 @@ val declare_summary : string -> 'a summary_declaration -> unit The [freeze_function] can be overridden *) val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref +val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag (* As [ref] but the value is local to a process, i.e. not sent to, say, proof * workers. It is useful to implement a local cache for example. *) @@ -55,10 +62,11 @@ module Local : sig end -(** Special name for the summary of ML modules. This summary entry is - special because its unfreeze may load ML code and hence add summary - entries. Thus is has to be recognizable, and handled appropriately *) -val ml_modules : string +(** Special summary for ML modules. This summary entry is special + because its unfreeze may load ML code and hence add summary + entries. Thus is has to be recognizable, and handled properly. + *) +val declare_ml_modules_summary : 'a summary_declaration -> unit (** For global tables registered statically before the end of coqtop launch, the following empty [init_function] could be used. *) @@ -72,19 +80,34 @@ type frozen val empty_frozen : frozen val freeze_summaries : marshallable:marshallable -> frozen -val unfreeze_summaries : frozen -> unit +val unfreeze_summaries : ?partial:bool -> frozen -> unit val init_summaries : unit -> unit -(** The type [frozen_bits] is a snapshot of some of the registered tables *) +(** Typed projection of the summary. Experimental API, use with CARE *) + +val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen +val project_from_summary : frozen -> 'a Dyn.tag -> 'a +val remove_from_summary : frozen -> 'a Dyn.tag -> frozen + +(** The type [frozen_bits] is a snapshot of some of the registered + tables. It is DEPRECATED in favor of the typed projection + version. *) + type frozen_bits +[@@ocaml.deprecated "Please use the typed version of summary projection"] -val freeze_summary : - marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits +[@@@ocaml.warning "-3"] +val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits +[@@ocaml.deprecated "Please use the typed version of summary projection"] val unfreeze_summary : frozen_bits -> unit +[@@ocaml.deprecated "Please use the typed version of summary projection"] val surgery_summary : frozen -> frozen_bits -> frozen +[@@ocaml.deprecated "Please use the typed version of summary projection"] val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits +[@@ocaml.deprecated "Please use the typed version of summary projection"] val pointer_equal : frozen_bits -> frozen_bits -> bool +[@@ocaml.deprecated "Please use the typed version of summary projection"] +[@@@ocaml.warning "+3"] (** {6 Debug} *) - val dump : unit -> (int * string) list diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8e6a01aa3..b766f0c6b 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -611,8 +611,8 @@ let unfreeze (grams, lex) = the lexer state should not be resetted, since it contains keywords declared in g_*.ml4 *) -let _ = - Summary.declare_summary "GRAMMAR_LEXER" +let parser_summary_tag = + Summary.declare_summary_tag "GRAMMAR_LEXER" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = Summary.nop } diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d17ccb0b4..3ca013a96 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -313,3 +313,6 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t + +type frozen_t +val parser_summary_tag : frozen_t Summary.Dyn.tag diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7..1f2e5f7ac 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2021,14 +2021,16 @@ let add_morphism glob binders m s n = (** Taken from original setoid_replace, to emulate the old rewrite semantics where lemmas are first instantiated and then rewrite proceeds. *) -let check_evar_map_of_evars_defs evd = +let check_evar_map_of_evars_defs env evd = let metas = Evd.meta_list evd in let check_freemetas_is_empty rebus = Evd.Metaset.iter (fun m -> - if Evd.meta_defined evd m then () else - raise - (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) + if Evd.meta_defined evd m then () + else begin + raise + (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m])) + end) in List.iter (fun (_,binding) -> @@ -2063,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in - check_evar_map_of_evars_defs sigma; + check_evar_map_of_evars_defs env sigma; let prf = nf prf in let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index e0d7eca5f..9e47db1c3 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index c36630f5d..6d5ee504e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -322,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) +let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ _ _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path x = !path_printer x +let print_path env sigma x = !path_printer env sigma x -let message_ambig l = - (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path ijp) l) +let message_ambig env sigma l = + str"Ambiguous paths:" ++ spc () ++ + prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -344,8 +344,8 @@ let different_class_params i = | CL_IND i -> Global.is_polymorphic (IndRef i) | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false - -let add_coercion_in_graph (ic,source,target) = + +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig !ambig_paths) + Feedback.msg_info (message_ambig env sigma !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -433,13 +433,13 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_, c) = +let cache_coercion env sigma (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; @@ -450,15 +450,15 @@ let cache_coercion (_, c) = coe_is_projection = c.coercion_is_proj; coe_param = c.coercion_params } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) + add_coercion_in_graph env sigma (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let open_coercion i o = if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -497,7 +497,9 @@ let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; - cache_function = cache_coercion; + cache_function = (fun objn -> + let env = Global.env () in cache_coercion env Evd.empty objn + ); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } diff --git a/pretyping/classops.mli b/pretyping/classops.mli index b41d0efac..47b41f17b 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -96,7 +96,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1eb2c31c8..647111bbe 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -903,18 +903,16 @@ let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path ((i,j),p) = - let sigma, env = Pfedit.get_current_context () in +let print_path env sigma ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j -(* XXX: This is suspicious!!! *) let _ = Classops.install_path_printer print_path -let print_graph () = - prlist_with_sep fnl print_path (inheritance_graph()) +let print_graph env sigma = + prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) @@ -929,7 +927,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between env sigma cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -940,7 +938,7 @@ let print_path_between cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path env sigma ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 8f3a6ddc4..fd7f1f92b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,6 +12,7 @@ open Reductionops open Libnames open Globnames open Misctypes +open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -39,10 +40,10 @@ val print_about : env -> Evd.evar_map -> reference or_by_notation -> val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> Pp.t +val print_graph : env -> evar_map -> Pp.t val print_classes : unit -> Pp.t val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) diff --git a/printing/printer.ml b/printing/printer.ml index 6a0597860..a63004ceb 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -905,7 +905,7 @@ end module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) -let pr_assumptionset env s = +let pr_assumptionset env sigma s = if ContextObjectMap.is_empty s && engagement env = PredicativeSet then str "Closed under the global context" @@ -921,7 +921,6 @@ let pr_assumptionset env s = with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = - let sigma, env = Pfedit.get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () diff --git a/printing/printer.mli b/printing/printer.mli index 36ca1bdcc..804014745 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -217,8 +217,7 @@ module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet -val pr_assumptionset : - env -> types ContextObjectMap.t -> Pp.t +val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 4a92c3856..8bd5d98cb 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,9 +54,10 @@ let clenv_value_cast_meta clenv = let clenv_pose_dependent_evars with_evars clenv = let dep_mvs = clenv_dependent clenv in + let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then raise - (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs (** Use our own fast path, more informative than from Typeclasses *) diff --git a/proofs/logic.ml b/proofs/logic.ml index a9ad606a0..1d86a0909 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -40,7 +40,7 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * Evd.evar_map * refiner_error open Pretype_errors @@ -69,7 +69,7 @@ let catchable_exception = function | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e | _ -> false -let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id)) +let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) @@ -78,10 +78,10 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp check sign id f = +let apply_to_hyp env sigma check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if check then error_no_such_hypothesis id + if check then error_no_such_hypothesis env sigma id else sign let check_typability env sigma c = @@ -147,7 +147,7 @@ let reorder_context env sigma sign ord = step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with - | [] -> error_no_such_hypothesis (List.hd ord) + | [] -> error_no_such_hypothesis env sigma (List.hd ord) | d :: ctxt -> let x = NamedDecl.get_id d in if Id.Set.mem x expected then @@ -190,9 +190,9 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let split_sign hfrom hto l = +let split_sign env sigma hfrom hto l = let rec splitrec left toleft = function - | [] -> error_no_such_hypothesis hfrom + | [] -> error_no_such_hypothesis env sigma hfrom | d :: right -> let hyp = NamedDecl.get_id d in if Id.equal hyp hfrom then @@ -222,7 +222,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then - error_no_such_hypothesis (hyp_of_move_location hto); + error_no_such_hypothesis env sigma (hyp_of_move_location hto); List.rev first @ List.rev middle | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> List.rev first @ List.rev middle @ right @@ -258,10 +258,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context sigma hfrom hto sign = +let move_hyp_in_named_context env sigma hfrom hto sign = let open EConstr in let (left,right,declfrom,toleft) = - split_sign hfrom hto (named_context_of_val sign) in + split_sign env sigma hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto let insert_decl_in_named_context sigma decl hto sign = @@ -293,15 +293,15 @@ let collect_meta_variables c = in List.rev (collrec false [] c) -let check_meta_variables c = +let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then - raise (RefinerError (NonLinearProof c)) + raise (RefinerError (env, sigma, NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = if !check then let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in if b then evm - else raise (RefinerError (BadType (arg,ty,conclty))) + else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list @@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Meta _ -> let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma conclty then - raise (RefinerError (MetaInType conclty)); + raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in let conclty = EConstr.Unsafe.to_constr conclty in @@ -477,7 +477,9 @@ and mk_arggoals sigma goal goalacc funty allargs = | Prod (_, c1, b) -> let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in (acc, subst1 harg b, sigma), arg - | _ -> raise (RefinerError (CannotApply (t, harg))) + | _ -> + let env = Goal.V82.env sigma goal in + raise (RefinerError (env,sigma,CannotApply (t, harg))) in Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs @@ -497,10 +499,10 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env() in + let env = Global.env () in let reorder = ref [] in let sign' = - apply_to_hyp check sign id + apply_to_hyp env sigma check sign id (fun _ d' _ -> let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in @@ -514,19 +516,18 @@ let convert_hyp check sign sigma d = map_named_decl EConstr.Unsafe.to_constr d) in reorder_val_context env sigma sign' !reorder - - (************************************************************************) (************************************************************************) (* Primitive tactics are handled here *) let prim_refiner r sigma goal = + let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in match r with (* Logical rules *) | Refine c -> let cl = EConstr.Unsafe.to_constr cl in - check_meta_variables c; + check_meta_variables env sigma c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in diff --git a/proofs/logic.mli b/proofs/logic.mli index 7df7fd66b..afd1ecf70 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -50,16 +50,16 @@ type refiner_error = | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * evar_map * refiner_error -val error_no_such_hypothesis : Id.t -> 'a +val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Evd.evar_map -> diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index cab8d7b52..d41541251 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -55,10 +55,11 @@ let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = + let env, sigma = pf_env gls, project gls in try Context.Named.lookup id (pf_hyps gls) with Not_found -> - raise (RefinerError (NoSuchHyp id)) + raise (RefinerError (env, sigma, NoSuchHyp id)) let pf_get_hyp_typ gls id = id |> pf_get_hyp gls |> NamedDecl.get_type @@ -182,9 +183,10 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.env gl in + let sigma = project gl in let sign = try EConstr.lookup_named id hyps - with Not_found -> raise (RefinerError (NoSuchHyp id)) + with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id)) in sign diff --git a/stm/stm.ml b/stm/stm.ml index b79a4a939..1d46e0833 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -187,9 +187,10 @@ let mkTransCmd cast cids ceff cqueue = Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } (* Parts of the system state that are morally part of the proof state *) -let summary_pstate = [ Evarutil.meta_counter_summary_name; - Evd.evar_counter_summary_name; - "program-tcc-table" ] +let summary_pstate = Evarutil.meta_counter_summary_tag, + Evd.evar_counter_summary_tag, + Obligations.program_tcc_summary_tag + type cached_state = | Empty | Error of Exninfo.iexn @@ -791,15 +792,21 @@ end = struct (* {{{ *) let fix_exn_ref = ref (fun x -> x) type proof_part = - Proof_global.t * Summary.frozen_bits (* only meta counters *) + Proof_global.t * + int * (* Evarutil.meta_counter_summary_tag *) + int * (* Evd.evar_counter_summary_tag *) + Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] let proof_part_of_frozen { Vernacstate.proof; system } = + let st = States.summary_of_state system in proof, - Summary.project_summary (States.summary_of_state system) summary_pstate + Summary.project_from_summary st Util.(pi1 summary_pstate), + Summary.project_from_summary st Util.(pi2 summary_pstate), + Summary.project_from_summary st Util.(pi3 summary_pstate) let freeze marshallable id = VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) @@ -859,16 +866,21 @@ end = struct (* {{{ *) else s with VCS.Expired -> s in VCS.set_state id (Valid s) - | `ProofOnly(ontop,(pstate,counters)) -> + | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system - (Summary.surgery_summary - (States.summary_of_state s.system) - counters) } in + begin + let st = States.summary_of_state s.system in + let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in + let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in + let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in + st + end + } in VCS.set_state id (Valid s) with VCS.Expired -> () @@ -883,10 +895,10 @@ end = struct (* {{{ *) let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in - let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in + let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in let s2 = States.summary_of_state s2 in - let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in - Summary.pointer_equal e1 e2 + let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in + e1 == e2 let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id @@ -2069,8 +2081,6 @@ and Reach : sig end = struct (* {{{ *) -let pstate = summary_pstate - let async_policy () = let open Flags in if is_universe_polymorphism () then false @@ -2283,10 +2293,14 @@ let known_state ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = - Summary.freeze_summary ~marshallable:`No ~complement:true pstate, - Lib.freeze ~marshallable:`No in + let st = Summary.freeze_summaries ~marshallable:`No in + let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in + st, Lib.freeze ~marshallable:`No in + let inject_non_pstate (s,l) = - Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () + Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = stm_purify (fun id -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index cee6d4bea..9e4d132d4 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -376,7 +376,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Proofview.Goal.enter begin fun gl -> let tacs = e_trivial_resolve db_list local_db secvars only_classes - (project gl) (pf_concl gl) in + (pf_env gl) (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) end in @@ -386,7 +386,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = in tclFIRST (List.map tclCOMPLETE tacl) -and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl = +and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl = let open Proofview.Notations in let prods, concl = EConstr.decompose_prod_assum sigma concl in let nprods = List.length prods in @@ -464,7 +464,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co in let tac = run_hint t tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in - let _, env = Pfedit.get_current_context () in let pp = match p with | Some pat when get_typeclasses_filtered_unification () -> @@ -476,16 +475,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db secvars only_classes sigma concl = +and e_trivial_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd true only_classes sigma concl + e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with Not_found -> [] -let e_possible_resolve db_list local_db secvars only_classes sigma concl = +let e_possible_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd false only_classes sigma concl + e_my_find_search db_list local_db secvars hd false only_classes env sigma concl with Not_found -> [] let cut_of_hints h = @@ -719,7 +718,7 @@ module V85 = struct let concl = Goal.V82.concl s gl in let tacgl = {it = gl; sigma = s;} in let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in - let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in + let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in let unique = is_unique env s concl in let rec aux i foundone = function | (tac, _, extern, name, pp) :: tl -> @@ -1072,7 +1071,7 @@ module Search = struct else str" without backtracking")); let secvars = compute_secvars gl in let poss = - e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in + e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f5c6ab879..d2e014e55 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -148,12 +148,12 @@ let rec e_trivial_fail_db db_list local_db = let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) + (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) end -and e_my_find_search sigma db_list local_db secvars hdc concl = +and e_my_find_search env sigma db_list local_db secvars hdc concl = let hint_of_db = hintmap_of sigma secvars hdc concl in let hintl = List.map_append (fun db -> @@ -178,20 +178,19 @@ and e_my_find_search sigma db_list local_db secvars hdc concl = | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in - let sigma, env = Pfedit.get_current_context () in (tac, lazy (pr_hint env sigma t))) in List.map tac_of_hint hintl -and e_trivial_resolve sigma db_list local_db secvars gl = +and e_trivial_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in - try priority (e_my_find_search sigma db_list local_db secvars hd gl) + try priority (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] -let e_possible_resolve sigma db_list local_db secvars gl = +let e_possible_resolve env sigma db_list local_db secvars gl = let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) - (e_my_find_search sigma db_list local_db secvars hd gl) + (e_my_find_search env sigma db_list local_db secvars hd gl) with Not_found -> [] let find_first_goal gls = @@ -291,7 +290,7 @@ module SearchProblem = struct let l = let concl = Reductionops.nf_evar (project g) (pf_concl g) in filter_tactics s.tacres - (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl) + (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl) in List.map (fun (lgls, cost, pp) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 0d6263246..22073d39b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1436,8 +1436,9 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let rec aux dest = function - | [] -> raise (RefinerError (NoSuchHyp id)) + | [] -> raise (RefinerError (env, sigma, NoSuchHyp id)) | d :: right -> let hyp = Context.Named.Declaration.get_id d in if Id.equal hyp id then dest else aux (MoveAfter hyp) right diff --git a/tactics/hints.ml b/tactics/hints.ml index 70e84013b..7f9b5ef34 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1400,15 +1400,10 @@ let pr_hint env sigma h = match h.obj with | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") - | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) + | Unfold_nth c -> + str"unfold " ++ pr_evaluable_reference c | Extern tac -> - let env = - try - let (_, env) = Pfedit.get_current_goal_context () in - env - with e when CErrors.noncritical e -> Global.env () - in - (str "(*external*) " ++ Pputils.pr_glb_generic env tac) + str "(*external*) " ++ Pputils.pr_glb_generic env tac let pr_id_hint env sigma (id, v) = let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in @@ -1507,6 +1502,7 @@ let pr_hint_db_env env sigma db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content +(* Deprecated in the mli *) let pr_hint_db db = let sigma, env = Pfedit.get_current_context () in pr_hint_db_env env sigma db diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e072bd95f..6aa052d32 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -187,7 +187,7 @@ let introduction ?(check=true) id = match EConstr.kind sigma concl with | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b - | _ -> raise (RefinerError IntroNeedsProduct) + | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end let refine = Tacmach.refine @@ -319,7 +319,7 @@ let move_hyp id dest = let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = named_context_val env in - let sign' = move_hyp_in_named_context sigma id dest sign in + let sign' = move_hyp_in_named_context env sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty @@ -348,13 +348,15 @@ let rename_hyp repl = let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in (** Check that we do not mess variables *) let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in let vars = List.fold_left fold Id.Set.empty hyps in let () = if not (Id.Set.subset src vars) then let hyp = Id.Set.choose (Id.Set.diff src vars) in - raise (RefinerError (NoSuchHyp hyp)) + raise (RefinerError (env, sigma, NoSuchHyp hyp)) in let mods = Id.Set.diff vars src in let () = @@ -442,9 +444,9 @@ let find_name mayrepl decl naming gl = match naming with (* Computing position of hypotheses for replacing *) (**************************************************************) -let get_next_hyp_position id = +let get_next_hyp_position env sigma id = let rec aux = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> if Id.equal (NamedDecl.get_id decl) id then match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst @@ -453,9 +455,9 @@ let get_next_hyp_position id = in aux -let get_previous_hyp_position id = +let get_previous_hyp_position env sigma id = let rec aux dest = function - | [] -> error_no_such_hypothesis id + | [] -> error_no_such_hypothesis env sigma id | decl :: right -> let hyp = NamedDecl.get_id decl in if Id.equal hyp id then dest else aux (MoveAfter hyp) right @@ -483,7 +485,7 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign = named_context_val env in let sign',t,concl,sigma = if replace then - let nexthyp = get_next_hyp_position id (named_context_of_val sign) in + let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma @@ -1000,6 +1002,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> @@ -1009,7 +1012,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | _ -> - begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct) + begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) (* this since at least V6.3 (a pity *) (* that intro do betaiotazeta only when reduction is needed; and *) @@ -1020,7 +1023,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = (Tacticals.New.tclTHEN hnf_in_concl (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end @@ -1059,7 +1062,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = (fun id -> aux (n+1) (id::ids)) end begin function (e, info) -> match e with - | RefinerError IntroNeedsProduct -> + | RefinerError (env, sigma, IntroNeedsProduct) -> tac ids | e -> Proofview.tclZERO ~info e end @@ -1070,8 +1073,9 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = let intro_replacing id = Proofview.Goal.enter begin fun gl -> + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let next_hyp = get_next_hyp_position id hyps in + let next_hyp = get_next_hyp_position env sigma id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; @@ -1090,8 +1094,9 @@ let intro_replacing id = let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> + let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (clear_for_replacing [id])) @@ -1105,7 +1110,8 @@ let intros_possibly_replacing ids = let intros_replacing ids = Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) @@ -2633,8 +2639,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) - else - get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in + else ( + let env, sigma = Proofview.Goal.(env gl, sigma gl) in + get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + ) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = @@ -4448,8 +4456,11 @@ let check_enough_applied env sigma elim = check_expected_type env sigma elimc elimt let guard_no_unifiable = Proofview.guard_no_unifiable >>= function -| None -> Proofview.tclUNIT () -| Some l -> Proofview.tclZERO (RefinerError (UnresolvedBindings l)) + | None -> Proofview.tclUNIT () + | Some l -> + Proofview.tclENV >>= function env -> + Proofview.tclEVARMAP >>= function sigma -> + Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l)) let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac = @@ -4648,7 +4659,7 @@ let induction_destruct isrec with_evars (lc,elim) = (Tacticals.New.tclMAP (fun (a,b,cl) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in + let sigma = Tacmach.New.project gl in onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag false with_evars None (a,b) cl) a end) l) @@ -4673,7 +4684,7 @@ let induction_destruct isrec with_evars (lc,elim) = end let induction ev clr c l e = - induction_gen clr true ev e + induction_gen clr true ev e ((Evd.empty,(c,NoBindings)),(None,l)) None let destruct ev clr c l e = diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 0f677a849..82b51b1ff 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -12,3 +12,5 @@ Check 0. Check S. Check nat. + +Type Type : Type. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index ac95ddd0c..82b04d132 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -221,13 +221,12 @@ Tactic Notation "extensionality" "in" hyp(H) := (* If we [subst H], things break if we already have another equation of the form [_ = H] *) destruct Heq; rename H_out into H. -(** Eta expansion follows from extensionality. *) +(** Eta expansion is built into Coq. *) Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) : f = fun x => f x. Proof. intros. - extensionality x. reflexivity. Qed. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 90db10ef1..237d878bf 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -22,15 +22,13 @@ Open Scope program_scope. Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. Proof. intros. - unfold id, compose. - symmetry. apply eta_expansion. + reflexivity. Qed. Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. Proof. intros. - unfold id, compose. - symmetry ; apply eta_expansion. + reflexivity. Qed. Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), @@ -47,9 +45,7 @@ Hint Rewrite <- @compose_assoc : core. Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id. Proof. - unfold flip, compose. intros. - extensionality x ; extensionality y ; extensionality z. reflexivity. Qed. @@ -57,9 +53,7 @@ Qed. Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id. Proof. - simpl ; intros. - unfold prod_uncurry, prod_curry, compose. - extensionality x ; extensionality y ; extensionality z. + intros. reflexivity. Qed. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 2dd559a95..209c22f71 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -40,6 +40,11 @@ Section Sets_as_an_algebra. auto 6 with sets. Qed. + Theorem Empty_set_zero_right : forall X:Ensemble U, Union U X (Empty_set U) = X. + Proof. + auto 6 with sets. + Qed. + Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. Proof. unfold Add at 1; auto using Empty_set_zero with sets. @@ -131,6 +136,17 @@ Section Sets_as_an_algebra. elim H'; intros x0 H'0; elim H'0; auto with sets. Qed. + Lemma Distributivity_l + : forall (A B C : Ensemble U), + Intersection U (Union U A B) C = + Union U (Intersection U A C) (Intersection U B C). + Proof. + intros A B C. + rewrite Intersection_commutative. + rewrite Distributivity. + f_equal; apply Intersection_commutative. + Qed. + Theorem Distributivity' : forall A B C:Ensemble U, Union U A (Intersection U B C) = @@ -251,6 +267,81 @@ Section Sets_as_an_algebra. intros; apply Definition_of_covers; auto with sets. Qed. + Lemma Disjoint_Intersection: + forall A s1 s2, Disjoint A s1 s2 -> Intersection A s1 s2 = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * destruct H. + intros x H1. unfold In in *. exfalso. intuition. apply (H _ H1). + * intuition. + Qed. + + Lemma Intersection_Empty_set_l: + forall A s, Intersection A (Empty_set A) s = Empty_set A. + Proof. + intros. auto with sets. + Qed. + + Lemma Intersection_Empty_set_r: + forall A s, Intersection A s (Empty_set A) = Empty_set A. + Proof. + intros. auto with sets. + Qed. + + Lemma Seminus_Empty_set_l: + forall A s, Setminus A (Empty_set A) s = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. destruct H1. unfold In in *. assumption. + * intuition. + Qed. + + Lemma Seminus_Empty_set_r: + forall A s, Setminus A s (Empty_set A) = s. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. destruct H1. unfold In in *. assumption. + * intuition. + Qed. + + Lemma Setminus_Union_l: + forall A s1 s2 s3, + Setminus A (Union A s1 s2) s3 = Union A (Setminus A s1 s3) (Setminus A s2 s3). + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H. inversion H. inversion H0; intuition. + * intros x H. constructor; inversion H; inversion H0; intuition. + Qed. + + Lemma Setminus_Union_r: + forall A s1 s2 s3, + Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H. inversion H. constructor. intuition. contradict H1. intuition. + * intros x H. inversion H. inversion H0. constructor; intuition. inversion H4; intuition. + Qed. + + Lemma Setminus_Disjoint_noop: + forall A s1 s2, + Intersection A s1 s2 = Empty_set A -> Setminus A s1 s2 = s1. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. inversion_clear H1. intuition. + * intros x H1. constructor; intuition. contradict H. + apply Inhabited_not_empty. + exists x. intuition. + Qed. + + Lemma Setminus_Included_empty: + forall A s1 s2, + Included A s1 s2 -> Setminus A s1 s2 = Empty_set A. + Proof. + intros. apply Extensionality_Ensembles. split. + * intros x H1. inversion_clear H1. contradiction H2. intuition. + * intuition. + Qed. + End Sets_as_an_algebra. Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7fd942908..6e87e67bb 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -289,13 +289,15 @@ ALLNATIVEFILES = \ $(OBJFILES:.o=.cmi) \ $(OBJFILES:.o=.cmx) \ $(OBJFILES:.o=.cmxs) -# trick: wildcard filters out non-existing files -NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) FILESTOINSTALL = \ $(VOFILES) \ $(VFILES) \ $(GLOBFILES) \ - $(NATIVEFILESTOINSTALL) \ + $(NATIVEFILES) \ $(CMIFILESTOINSTALL) BYTEFILESTOINSTALL = \ $(CMOFILESTOINSTALL) \ @@ -535,7 +537,7 @@ clean:: $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) @@ -563,7 +565,7 @@ cleanall:: clean archclean:: @# Extension point $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) .PHONY: archclean diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 3a8e8fb43..d328ad0cf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -75,8 +75,7 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> - let sigma, env = Pfedit.get_current_context () in + | Logic.RefinerError (env, sigma, e) -> wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d3de10235..00554e3ba 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -378,7 +378,7 @@ let unfreeze_ml_modules x = (fun (name,path) -> trigger_ml_object false false false ?path name) x let _ = - Summary.declare_summary Summary.ml_modules + Summary.declare_ml_modules_summary { Summary.freeze_function = (fun _ -> get_loaded_modules ()); Summary.unfreeze_function = unfreeze_ml_modules; Summary.init_function = reset_loaded_modules } diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4f011e6ad..181068089 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let from_prg : program_info ProgMap.t ref = - Summary.ref ProgMap.empty ~name:"program-tcc-table" +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" let close sec = if not (ProgMap.is_empty !from_prg) then diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 0602e52e9..bdc97d48c 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -104,3 +104,6 @@ exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t val set_program_mode : bool -> unit + +type program_info +val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 6a10eb43a..7e96f28de 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -288,7 +288,6 @@ let init_terminal_output ~color = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning - (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in @@ -311,17 +310,23 @@ let print_err_exn ?extra any = std_logger ~pre_hdr Feedback.Error msg let with_output_to_file fname func input = - (* XXX FIXME: redirect std_ft *) - (* let old_logger = !logger in *) let channel = open_out (String.concat "." [fname; "out"]) in - (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *) + let old_fmt = !std_ft, !err_ft, !deep_ft in + let new_ft = Format.formatter_of_out_channel channel in + std_ft := new_ft; + err_ft := new_ft; + deep_ft := new_ft; try let output = func input in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; output with reraise -> let reraise = Backtrace.add_backtrace reraise in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 63768d9b8..161e0c535 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1591,13 +1591,14 @@ let vernac_declare_reduction ~atts s r = let vernac_global_check c = let env = Global.env() in let sigma = Evd.from_env env in - let c,ctx = interp_constr env sigma c in + let c,uctx = interp_constr env sigma c in let senv = Global.safe_env() in - let cstrs = snd (UState.context_set ctx) in - let senv = Safe_typing.add_constraints cstrs senv in + let uctx = UState.context_set uctx in + let senv = Safe_typing.push_context_set false uctx senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - Feedback.msg_notice (print_safe_judgment env sigma j) + Feedback.msg_notice (print_safe_judgment env sigma j ++ + pr_universe_ctx_set sigma uctx) let get_nth_goal n = @@ -1656,13 +1657,13 @@ let vernac_print ~atts env sigma = | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph()) + | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) + msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -1696,7 +1697,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) + msg_notice (Printer.pr_assumptionset env sigma nassums) | PrintStrategy r -> print_strategy r let global_module r = |