diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-09 10:31:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-09 10:31:13 +0200 |
| commit | eb7da0d0a02a406c196214ec9d08384385541788 (patch) | |
| tree | efe031d7df32573abd7b39afa0f009a6d61f18d5 | |
| parent | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (diff) | |
| parent | 73daf37ccc7a44cd29c9b67405111756c75cb26a (diff) | |
Merge branch 'v8.5'
81 files changed, 799 insertions, 307 deletions
@@ -35,6 +35,8 @@ Program - The "Shrink Obligations" flag now applies to all obligations, not only those solved by the automatic tactic. +- Importing Program no longer overrides the "exists" tactic (potential source + of incompatibilities). API diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 7af87a399..5dbf31553 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -157,6 +157,14 @@ in Section~\ref{ProofWith}. Use only section variables occurring in the statement. +\variant {\tt Proof using Type*.} + + The {\tt *} operator computes the forward transitive closure. + E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is + in {\tt p*} since {\tt p} occurs in the type of {\tt H}. + {\tt Type* } is the forward transitive closure of the entire set of + section variables occurring in the statement. + \variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}. @@ -164,14 +172,18 @@ in Section~\ref{ProofWith}. \variant {\tt Proof using } {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .} \variant {\tt Proof using } {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .} \variant {\tt Proof using } {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} +\variant {\tt Proof using } {\emph collection$_1$}{\tt* .} - Use section variables being in the set union or set difference of the two - colelctions. See Section~\ref{Collection} to know how to form a named + Use section variables being, respectively, in the set union, set difference, + set complement, set forward transitive closure. + See Section~\ref{Collection} to know how to form a named collection. + The {\tt *} operator binds stronger than {\tt +} and {\tt -}. \subsubsection{{\tt Proof using} options} -\comindex{Default Proof Using} -\comindex{Suggest Proof Using} +\optindex{Default Proof Using} +\optindex{Suggest Proof Using} +\optindex{Proof Using Clear Unused} The following options modify the behavior of {\tt Proof using}. @@ -186,11 +198,17 @@ The following options modify the behavior of {\tt Proof using}. When {\tt Qed} is performed, suggest a {\tt using} annotation if the user did not provide one. +\variant{\tt Unset Proof Using Clear Unused.} + + When {\tt Proof using a} all section variables but for {\tt a} and + the variables used in the type of {\tt a} are cleared. + This option can be used to turn off this behavior. + \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}} \comindex{Collection}\label{Collection} The command {\tt Collection} can be used to name a set of section hypotheses, -with the purpose of making {\tt Proof using} annotations more compat. +with the purpose of making {\tt Proof using} annotations more compact. \variant {\tt Collection Some := x y z.} @@ -209,7 +227,7 @@ with the purpose of making {\tt Proof using} annotations more compat. \variant {\tt Collection Many := Fewer - (x y).} Define the collection named "Many" containing the set difference - of "Fewer" and the unamed collection {\tt x y}. + of "Fewer" and the unnamed collection {\tt x y}. \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}} diff --git a/engine/evd.ml b/engine/evd.ml index 3f4bfe7af..64aad8082 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1021,8 +1021,8 @@ let merge_uctx sideff rigid uctx ctx' = let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } -let merge_context_set rigid evd ctx' = - {evd with universes = merge_uctx false rigid evd.universes ctx'} +let merge_context_set ?(sideff=false) rigid evd ctx' = + {evd with universes = merge_uctx sideff rigid evd.universes ctx'} let merge_uctx_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } @@ -1067,12 +1067,6 @@ let uctx_new_univ_variable rigid name predicative uctx_univ_algebraic = Univ.LSet.add u avars}, false else {uctx with uctx_univ_variables = uvars'}, false in - (* let ctx' = *) - (* if pred then *) - (* Univ.ContextSet.add_constraints *) - (* (Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *) - (* else ctx' *) - (* in *) let names = match name with | Some n -> add_uctx_names n u uctx.uctx_names @@ -1323,8 +1317,7 @@ let normalize_evar_universe_context uctx = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic in - if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then - uctx + if Univ.ContextSet.equal us' uctx.uctx_local then uctx else let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in let uctx' = diff --git a/engine/evd.mli b/engine/evd.mli index 22d017497..d659b8826 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -538,7 +538,7 @@ val universes : evar_map -> UGraph.t val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map -val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index c28ed6860..1dcef22b9 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -292,11 +292,13 @@ let export_option_value = function | Goptions.BoolValue b -> Interface.BoolValue b | Goptions.IntValue x -> Interface.IntValue x | Goptions.StringValue s -> Interface.StringValue s + | Goptions.StringOptValue s -> Interface.StringOptValue s let import_option_value = function | Interface.BoolValue b -> Goptions.BoolValue b | Interface.IntValue x -> Goptions.IntValue x | Interface.StringValue s -> Goptions.StringValue s + | Interface.StringOptValue s -> Goptions.StringOptValue s let export_option_state s = { Interface.opt_sync = s.Goptions.opt_sync; @@ -315,6 +317,8 @@ let set_options options = | BoolValue b -> Goptions.set_bool_option_value name b | IntValue i -> Goptions.set_int_option_value name i | StringValue s -> Goptions.set_string_option_value name s + | StringOptValue (Some s) -> Goptions.set_string_option_value name s + | StringOptValue None -> Goptions.unset_option_value_gen None name in List.iter iter options diff --git a/ide/interface.mli b/ide/interface.mli index f3777ba36..f2f121ac0 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -62,6 +62,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 7445ce5ca..32c39e20d 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -62,10 +62,12 @@ let of_option_value = function | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b] | StringValue s -> constructor "option_value" "stringvalue" [of_string s] + | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s] let to_option_value = do_match "option_value" (fun s args -> match s with | "intvalue" -> IntValue (to_option to_int (singleton args)) | "boolvalue" -> BoolValue (to_bool (singleton args)) | "stringvalue" -> StringValue (to_string (singleton args)) + | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args)) | _ -> raise Marshal_error) let of_option_state s = @@ -337,6 +339,8 @@ end = struct | IntValue None -> "none" | IntValue (Some i) -> string_of_int i | StringValue s -> s + | StringOptValue None -> "none" + | StringOptValue (Some s) -> s | BoolValue b -> if b then "true" else "false" let pr_option_state (s : option_state) = Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 74e136904..5c11119ed 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -44,8 +44,8 @@ type 'id move_location = (** Sorts *) type 'a glob_sort_gen = GProp | GSet | GType of 'a -type sort_info = string list -type level_info = string option +type sort_info = string Loc.located list +type level_info = string Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 37218fbf9..f89f076b5 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -155,6 +155,7 @@ type option_value = Goptions.option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option type option_ref_value = | StringRefValue of string @@ -224,12 +225,12 @@ type scheme = | EqualityScheme of reference or_by_notation type section_subset_expr = - | SsSet of lident list + | SsEmpty + | SsSingl of lident | SsCompl of section_subset_expr | SsUnion of section_subset_expr * section_subset_expr | SsSubstr of section_subset_expr * section_subset_expr - -type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr + | SsFwdClose of section_subset_expr (** Extension identifiers for the VERNAC EXTEND mechanism. *) type extend_name = @@ -313,7 +314,7 @@ type vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * - inline * simple_binder with_coercion list + inline * (plident list * constr_expr) with_coercion list | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list @@ -335,7 +336,7 @@ type vernac_expr = class_rawexpr * class_rawexpr | VernacIdentityCoercion of obsolete_locality * lident * class_rawexpr * class_rawexpr - | VernacNameSectionHypSet of lident * section_subset_descr + | VernacNameSectionHypSet of lident * section_subset_expr (* Type classes *) | VernacInstance of @@ -440,7 +441,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_descr option + | VernacProof of raw_tactic_expr option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 926b38794..b6df8f454 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -182,14 +182,17 @@ let global_vars_set_constant_type env = function (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty -let record_aux env s1 s2 = +let record_aux env s_ty s_bo suggested_expr = + let in_ty = keep_hyps env s_ty in let v = String.concat " " - (List.map (fun (id, _,_) -> Id.to_string id) - (keep_hyps env (Id.Set.union s1 s2))) in - Aux_file.record_in_aux "context_used" v + (CList.map_filter (fun (id, _,_) -> + if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None + else Some (Id.to_string id)) + (keep_hyps env s_bo)) in + Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) -let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) +let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = @@ -204,6 +207,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) str " " ++ str (String.conjugate_verb_to_be n) ++ str " used but not declared:" ++ fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in + let sort evn l = + List.filter (fun (id,_,_) -> + List.exists (fun (id',_,_) -> Names.Id.equal id id') l) + (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map pi1 (named_context env) in @@ -221,19 +228,21 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (Opaqueproof.force_proof (opaque_tables env) lc) in (* we force so that cst are added to the env immediately after *) ignore(Opaqueproof.force_constraints (opaque_tables env) lc); - !suggest_proof_using kn env vars ids_typ context_ids; + let expr = + !suggest_proof_using (Constant.to_string kn) + env vars ids_typ context_ids in if !Flags.compilation_mode = Flags.BuildVo then - record_aux env ids_typ vars; + record_aux env ids_typ vars expr; vars in keep_hyps env (Idset.union ids_typ ids_def), def | None -> if !Flags.compilation_mode = Flags.BuildVo then - record_aux env Id.Set.empty Id.Set.empty; + record_aux env Id.Set.empty Id.Set.empty ""; [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) - declared, + sort env declared, match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> @@ -303,6 +312,20 @@ let translate_local_def env id centry = let def,typ,proj,poly,univs,inline_code,ctx = infer_declaration env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in + if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin + match def with + | Undef _ -> () + | Def _ -> () + | OpaqueDef lc -> + let context_ids = List.map pi1 (named_context env) in + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env + (Opaqueproof.force_proof (opaque_tables env) lc) in + let expr = + !suggest_proof_using (Id.to_string id) + env ids_def ids_typ context_ids in + record_aux env ids_typ ids_def expr + end; def, typ, univs (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1b54b1ea1..8d92bcc68 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -44,4 +44,4 @@ val build_constant_declaration : constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : - (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit + (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index 7e6d4de23..8201980e3 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1020,6 +1020,9 @@ struct let empty = (LSet.empty, Constraint.empty) let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst + let equal (univs, cst as x) (univs', cst' as y) = + x == y || (LSet.equal univs univs' && Constraint.equal cst cst') + let of_set s = (s, Constraint.empty) let singleton l = of_set (LSet.singleton l) let of_instance i = of_set (Instance.levels i) diff --git a/kernel/univ.mli b/kernel/univ.mli index dbbc83262..ae7400337 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -325,6 +325,7 @@ sig val of_instance : Instance.t -> t val of_set : universe_set -> t + val equal : t -> t -> bool val union : t -> t -> t val append : t -> t -> t diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c9018c9ee..5dedb0d0a 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -42,6 +42,8 @@ module M = Map.Make(String) type data = string M.t type aux_file = data H.t +let contents x = x + let empty_aux_file = H.empty let get aux loc key = M.find key (H.find (Loc.unloc loc) aux) diff --git a/lib/aux_file.mli b/lib/aux_file.mli index e340fc654..b672d3db2 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string val empty_aux_file : aux_file val set : aux_file -> Loc.t -> string -> string -> aux_file +module H : Map.S with type key = int * int +module M : Map.S with type key = string +val contents : aux_file -> string M.t H.t + val start_aux_file_for : string -> unit val stop_aux_file : unit -> unit val recording : unit -> bool diff --git a/lib/cThread.ml b/lib/cThread.ml index 2d1f10bf3..9cbdf5a9e 100644 --- a/lib/cThread.ml +++ b/lib/cThread.ml @@ -8,22 +8,12 @@ type thread_ic = in_channel -let prepare_in_channel_for_thread_friendly_io ic = - Unix.set_nonblock (Unix.descr_of_in_channel ic); ic - -let safe_wait_timed_read fd time = - try Thread.wait_timed_read fd time - with Unix.Unix_error (Unix.EINTR, _, _) -> - (** On Unix, the above function may raise this exception when it is - interrupted by a signal. (It uses Unix.select internally.) *) - false +let prepare_in_channel_for_thread_friendly_io ic = ic let thread_friendly_read_fd fd s ~off ~len = let rec loop () = try Unix.read fd s off len - with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) -> - while not (safe_wait_timed_read fd 0.05) do Thread.yield () done; - loop () + with Unix.Unix_error(Unix.EINTR,_,_) -> loop () in loop () diff --git a/lib/future.ml b/lib/future.ml index 02d3702d7..78a158264 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -11,21 +11,27 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t) let unfreeze = ref (fun _ -> () : Dyn.t -> unit) let set_freeze f g = freeze := f; unfreeze := g -exception NotReady of string -exception NotHere of string -let _ = Errors.register_handler (function - | NotReady name -> +let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ "asynchronous script processing and don't pass \"-quick\" to "^ - "coqc.") - | NotHere name -> + "coqc.")) +let not_here_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not available "^ "in this process. If you really need this, pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ "asynchronous script processing and don't pass \"-quick\" to "^ - "coqc.") + "coqc.")) + +let customize_not_ready_msg f = not_ready_msg := f +let customize_not_here_msg f = not_here_msg := f + +exception NotReady of string +exception NotHere of string +let _ = Errors.register_handler (function + | NotReady name -> !not_ready_msg name + | NotHere name -> !not_here_msg name | _ -> raise Errors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn diff --git a/lib/future.mli b/lib/future.mli index 324d5f7d1..de2282ae9 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds Thy are set for the outermos layer of the system, since they have to deal with the whole system state. *) val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit + +val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit +val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit diff --git a/lib/spawn.ml b/lib/spawn.ml index 9b63be70a..851c6a223 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -45,26 +45,38 @@ end (* Common code *) let assert_ b s = if not b then Errors.anomaly (Pp.str s) +(* According to http://caml.inria.fr/mantis/view.php?id=5325 + * you can't use the same socket for both writing and reading (may change + * in 4.03 *) let mk_socket_channel () = let open Unix in - let s = socket PF_INET SOCK_STREAM 0 in - bind s (ADDR_INET (inet_addr_loopback,0)); - listen s 1; - match getsockname s with - | ADDR_INET(host, port) -> - s, string_of_inet_addr host ^":"^ string_of_int port + let sr = socket PF_INET SOCK_STREAM 0 in + bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1; + let sw = socket PF_INET SOCK_STREAM 0 in + bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1; + match getsockname sr, getsockname sw with + | ADDR_INET(host, portr), ADDR_INET(_, portw) -> + (sr, sw), + string_of_inet_addr host + ^":"^ string_of_int portr ^":"^ string_of_int portw | _ -> assert false -let accept s = - let r, _, _ = Unix.select [s] [] [] accept_timeout in +let accept (sr,sw) = + let r, _, _ = Unix.select [sr] [] [] accept_timeout in if r = [] then raise (Failure (Printf.sprintf "The spawned process did not connect back in %2.1fs" accept_timeout)); - let cs, _ = Unix.accept s in - Unix.close s; - let cin, cout = Unix.in_channel_of_descr cs, Unix.out_channel_of_descr cs in + let csr, _ = Unix.accept sr in + Unix.close sr; + let cin = Unix.in_channel_of_descr csr in set_binary_mode_in cin true; + let w, _, _ = Unix.select [sw] [] [] accept_timeout in + if w = [] then raise (Failure (Printf.sprintf + "The spawned process did not connect back in %2.1fs" accept_timeout)); + let csw, _ = Unix.accept sw in + Unix.close sw; + let cout = Unix.out_channel_of_descr csw in set_binary_mode_out cout true; - cs, cin, cout + (csr, csw), cin, cout let handshake cin cout = try @@ -116,7 +128,7 @@ let spawn_pipe env prog args = let cout = Unix.out_channel_of_descr master2worker_w in set_binary_mode_in cin true; set_binary_mode_out cout true; - pid, cin, cout, worker2master_r + pid, cin, cout, (worker2master_r, master2worker_w) let filter_args args = let rec aux = function @@ -180,10 +192,10 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) = let pid, oob_resp, oob_req, cin, cout, main, is_sock = spawn_with_control prefer_sock env prog args in - Unix.set_nonblock main; + Unix.set_nonblock (fst main); let gchan = - if is_sock then ML.async_chan_of_socket main - else ML.async_chan_of_file main in + if is_sock then ML.async_chan_of_socket (fst main) + else ML.async_chan_of_file (fst main) in let alive, watch = true, None in let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in p.watch <- Some ( diff --git a/library/goptions.ml b/library/goptions.ml index 4f50fbfbd..30d195f83 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -20,6 +20,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { @@ -293,6 +294,10 @@ let declare_string_option = declare_option (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) +let declare_stringopt_option = + declare_option + (fun v -> StringOptValue v) + (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option")) (* 3- User accessible commands *) @@ -324,11 +329,13 @@ let check_bool_value v = function let check_string_value v = function | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) | _ -> bad_type_error () let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None + | StringOptValue _ -> StringOptValue None | _ -> bad_type_error () (* Nota: For compatibility reasons, some errors are treated as @@ -359,6 +366,8 @@ let msg_option_value (name,v) = | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s + | StringOptValue None -> str"undefined" + | StringOptValue (Some s) -> str s (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = diff --git a/library/goptions.mli b/library/goptions.mli index 1c44f8908..9d87c14c5 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -128,6 +128,7 @@ type 'a write_function = 'a -> unit val declare_int_option : int option option_sig -> int option write_function val declare_bool_option : bool option_sig -> bool write_function val declare_string_option: string option_sig -> string write_function +val declare_stringopt_option: string option option_sig -> string option write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) @@ -165,6 +166,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { diff --git a/library/universes.ml b/library/universes.ml index 067558c8a..fe5730e95 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -26,6 +26,11 @@ let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd !global_universes)) with Not_found -> Level.pr l +(* To disallow minimization to Set *) + +let set_minimization = ref true +let is_set_minimization () = !set_minimization + type universe_constraint_type = ULe | UEq | ULub type universe_constraint = universe * universe_constraint_type * universe @@ -832,7 +837,9 @@ let normalize_context_set ctx us algs = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> if d == Le then if Univ.Level.is_small l then - (Constraint.add cstr smallles, noneqs) + if is_set_minimization () then + (Constraint.add cstr smallles, noneqs) + else (smallles, noneqs) else if Level.is_small r then if Level.is_prop r then raise (Univ.UniverseInconsistency @@ -872,6 +879,8 @@ let normalize_context_set ctx us algs = if d == Eq then (UF.union l r uf; noneqs) else (* We ignore the trivial Prop/Set <= i constraints. *) if d == Le && Univ.Level.is_small l then noneqs + else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r + then noneqs else Constraint.add cstr noneqs) csts Constraint.empty in diff --git a/library/universes.mli b/library/universes.mli index c897a88a9..cfa0ad0c1 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -12,6 +12,9 @@ open Term open Environ open Univ +val set_minimization : bool ref +val is_set_minimization : unit -> bool + (** Universes *) type universe_names = diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index e47e3fb1e..e2e6795f7 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -153,12 +153,12 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType [] - | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u) + | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u) ] ] ; universe: - [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids - | id = ident -> [id] + [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids + | id = identref -> [id] ] ] ; lconstr: @@ -224,11 +224,20 @@ GEXTEND Gram ] ] ; record_declaration: - [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs) + [ [ fs = record_fields -> CRecord (!@loc, None, fs) (* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) (* CRecord (!@loc, Some c, fs) *) ] ] ; + + record_fields: + [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs + | f = record_field_declaration; ";" -> [f] + | f = record_field_declaration -> [f] + | -> [] + ] ] + ; + record_field_declaration: [ [ id = global; params = LIST0 identref; ":="; c = lconstr -> (id, abstract_constr_expr c (binders_of_lidents params)) ] ] @@ -302,7 +311,7 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None - | id = ident -> GType (Some (Id.to_string id)) + | id = identref -> GType (Some (fst id, Id.to_string (snd id))) ] ] ; fix_constr: @@ -356,9 +365,16 @@ GEXTEND Gram [ [ pll = LIST1 mult_pattern SEP "|"; "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ] ; - recordpattern: + record_pattern: [ [ id = global; ":="; pat = pattern -> (id, pat) ] ] ; + record_patterns: + [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps + | p = record_pattern; ";" -> [p] + | p = record_pattern-> [p] + | -> [] + ] ] + ; pattern: [ "200" RIGHTA [ ] | "100" RIGHTA @@ -382,7 +398,7 @@ GEXTEND Gram [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ] | "0" [ r = Prim.reference -> CPatAtom (!@loc,Some r) - | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat) + | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat) | "_" -> CPatAtom (!@loc,None) | "("; p = pattern LEVEL "200"; ")" -> (match p with diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1e254c16b..7f5459bfa 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -37,12 +37,12 @@ GEXTEND Gram command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c | IDENT "Proof" -> - VernacProof (None,hint_proof_using G_vernac.section_subset_descr None) + VernacProof (None,hint_proof_using G_vernac.section_subset_expr None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; "with"; ta = tactic; - l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] -> - VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l) - | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr; + l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> + VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l) + | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; ta = OPT [ "with"; ta = tactic -> ta ] -> VernacProof (ta,Some l) | IDENT "Proof"; c = lconstr -> VernacExactProof c diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 63850713f..1f9f57f69 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -46,7 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field" let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" -let section_subset_descr = Gram.entry_create "vernac:section_subset_descr" +let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" let command_entry = ref noedit_mode let set_command_entry e = command_entry := e @@ -269,7 +269,7 @@ GEXTEND Gram | -> NoInline] ] ; pidentref: - [ [ i = identref; l = OPT [ "@{" ; l = LIST1 identref; "}" -> l ] -> (i,l) ] ] + [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] ; univ_constraint: [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; @@ -325,9 +325,9 @@ GEXTEND Gram | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> Constructors ((c id)::l) | id = identref ; c = constructor_type -> Constructors [ c id ] - | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> + | cstr = identref; "{"; fs = record_fields; "}" -> RecordDecl (Some cstr,fs) - | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) + | "{";fs = record_fields; "}" -> RecordDecl (None,fs) | -> Constructors [] ] ] ; (* @@ -389,6 +389,13 @@ GEXTEND Gram [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; ntn = decl_notation -> (bd,pri),ntn ] ] ; + record_fields: + [ [ f = record_field; ";"; fs = record_fields -> f :: fs + | f = record_field; ";" -> [f] + | f = record_field -> [f] + | -> [] + ] ] + ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t)) @@ -413,7 +420,7 @@ GEXTEND Gram [ [ "("; a = simple_assum_coe; ")" -> a ] ] ; simple_assum_coe: - [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> + [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr -> (not (Option.is_empty oc),(idl,c)) ] ] ; @@ -440,20 +447,24 @@ GEXTEND Gram ; END -let only_identrefs = - Gram.Entry.of_parser "test_only_identrefs" +let only_starredidentrefs = + Gram.Entry.of_parser "test_only_starredidentrefs" (fun strm -> let rec aux n = match get_tok (Util.stream_nth n strm) with | KEYWORD "." -> () | KEYWORD ")" -> () - | IDENT _ -> aux (n+1) + | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) | _ -> raise Stream.Failure in aux 0) +let starredidentreflist_to_expr l = + match l with + | [] -> SsEmpty + | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x (* Modules and Sections *) GEXTEND Gram - GLOBAL: gallina_ext module_expr module_type section_subset_descr; + GLOBAL: gallina_ext module_expr module_type section_subset_expr; gallina_ext: [ [ (* Interactive module declaration *) @@ -476,7 +487,7 @@ GEXTEND Gram | IDENT "End"; id = identref -> VernacEndSegment id (* Naming a set of section hyps *) - | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr -> + | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr -> VernacNameSectionHypSet (id, expr) (* Requiring an already compiled module *) @@ -567,22 +578,32 @@ GEXTEND Gram CMwith (!@loc,mty,decl) ] ] ; - section_subset_descr: - [ [ IDENT "All" -> SsAll - | "Type" -> SsType - | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l) - | e = section_subset_expr -> SsExpr e ] ] - ; + (* Proof using *) section_subset_expr: + [ [ only_starredidentrefs; l = LIST0 starredidentref -> + starredidentreflist_to_expr l + | e = ssexpr -> e ]] + ; + starredidentref: + [ [ i = identref -> SsSingl i + | i = identref; "*" -> SsFwdClose(SsSingl i) + | "Type" -> SsSingl (!@loc, Id.of_string "Type") + | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]] + ; + ssexpr: [ "35" - [ "-"; e = section_subset_expr -> SsCompl e ] + [ "-"; e = ssexpr -> SsCompl e ] | "50" - [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2) - | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)] + [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2) + | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)] | "0" - [ i = identref -> SsSet [i] - | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l - | "("; e = section_subset_expr; ")"-> e ] ] + [ i = starredidentref -> i + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> + starredidentreflist_to_expr l + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> + SsFwdClose(starredidentreflist_to_expr l) + | "("; e = ssexpr; ")"-> e + | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ] ; END diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6439f58d2..068cb25cf 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -482,19 +482,28 @@ let congruence_tac depth l = This isn't particularly related with congruence, apart from the fact that congruence is called internally. *) - + +let mk_eq f c1 c2 k = + Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> + Proofview.Goal.enter begin + fun gl -> + let open Tacmach.New in + let evm, ty = pf_apply type_of gl c1 in + let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in + let term = mkApp (fc, [| ty; c1; c2 |]) in + let evm, _ = type_of (pf_env gl) evm term in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) + (k term) + end) + let f_equal = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let type_of = Tacmach.New.pf_unsafe_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) - let ty = (* Termops.refresh_universes *) (type_of c1) in - if eq_constr_nounivs c1 c2 then Proofview.tclUNIT () - else - Tacticals.New.tclTRY (Tacticals.New.tclTHEN - ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) - (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))) + Tacticals.New.tclTHEN + (mk_eq _eq c1 c2 Tactics.cut) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 05e09b968..2a4be9f31 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1865,7 +1865,14 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) -let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = +let context_of_arsign l = + let (x, _) = List.fold_right + (fun c (x, n) -> + (lift_rel_context n c @ x, List.length c + n)) + l ([], 0) + in x + +let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in let subst, len = List.fold_left2 (fun (subst, len) (tm, tmtype) sign -> @@ -1905,7 +1912,9 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = mkRel (n + nar)) | _ -> map_constr_with_binders succ predicate lift c - in predicate 0 c + in + let p = predicate 0 c in + fst (Typing.type_of (push_rel_context (context_of_arsign arsign) env) sigma p), p (* Builds the predicate. If the predicate is dependent, its context is @@ -1927,11 +1936,11 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) (* First strategy: we abstract the tycon wrt to the dependencies *) - let pred1 = - prepare_predicate_from_arsign_tycon loc tomatchs arsign t in + let sigma1,pred1 = + prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in - [sigma, pred1; sigma2, pred2] + [sigma1, pred1; sigma2, pred2] | None, _ -> (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) @@ -2366,13 +2375,6 @@ let build_dependent_signature env evdref avoid tomatchs arsign = assert(Int.equal slift 0); (* we must have folded over all elements of the arity signature *) arsign'', allnames, nar, eqs, neqs, refls -let context_of_arsign l = - let (x, _) = List.fold_right - (fun c (x, n) -> - (lift_rel_context n c @ x, List.length c + n)) - l ([], 0) - in x - let compile_program_cases loc style (typing_function, evdref) tycon env (predopt, tomatchl, eqns) = let typing_fun tycon env = function @@ -2404,10 +2406,8 @@ let compile_program_cases loc style (typing_function, evdref) tycon env | Some t -> let pred = try - let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in - (* The tycon may be ill-typed after abstraction. *) - let env' = push_rel_context (context_of_arsign sign) env in - ignore(Typing.sort_of env' evdref pred); pred + let evd, pred = prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t in + evdref := evd; pred with e when Errors.noncritical e -> let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8bd57290b..a1213e72b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -401,7 +401,7 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)] + then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -413,7 +413,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l))) + GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l))) let detype_instance sigma l = if Univ.Instance.is_empty l then None diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 0926e7a29..a0ec1baae 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,7 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.equal CString.equal l1 l2 +| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6373e6079..17eafb19e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -99,8 +99,31 @@ let search_guard loc env possible_indexes fixdefs = let ((constr_in : constr -> Dyn.t), (constr_out : Dyn.t -> constr)) = Dyn.create "constr" +(* To force universe name declaration before use *) + +let strict_universe_declarations = ref true +let is_strict_universe_declarations () = !strict_universe_declarations + +let _ = + Goptions.(declare_bool_option + { optsync = true; + optdepr = false; + optname = "strict universe declaration"; + optkey = ["Strict";"Universe";"Declaration"]; + optread = is_strict_universe_declarations; + optwrite = (:=) strict_universe_declarations }) + +let _ = + Goptions.(declare_bool_option + { optsync = true; + optdepr = false; + optname = "minimization to Set"; + optkey = ["Universe";"set";"Minimization"]; + optread = Universes.is_set_minimization; + optwrite = (:=) Universes.set_minimization }) + (** Miscellaneous interpretation functions *) -let interp_universe_level_name evd s = +let interp_universe_level_name evd (loc,s) = let names, _ = Universes.global_universe_names () in if CString.string_contains s "." then match List.rev (CString.split '.' s) with @@ -122,7 +145,10 @@ let interp_universe_level_name evd s = try let level = Evd.universe_of_name evd s in evd, level with Not_found -> - new_univ_level_variable ~name:s univ_rigid evd + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ~name:s univ_rigid evd + else user_err_loc (loc, "interp_universe_level_name", + Pp.(str "Undeclared universe: " ++ str s)) let interp_universe evd = function | [] -> let evd, l = new_univ_level_variable univ_rigid evd in @@ -135,7 +161,7 @@ let interp_universe evd = function let interp_universe_level evd = function | None -> new_univ_level_variable univ_rigid evd - | Some s -> interp_universe_level_name evd s + | Some (loc,s) -> interp_universe_level_name evd (loc,s) let interp_sort evd = function | GProp -> evd, Prop Null @@ -357,7 +383,8 @@ let evar_kind_of_term sigma c = (*************************************************************************) (* Main pretyping function *) -let interp_universe_level_name evd = function +let interp_universe_level_name evd l = + match l with | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set | GType s -> interp_universe_level evd s diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 650b8f726..ea705e335 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -140,8 +140,8 @@ end) = struct let pr_univ l = match l with - | [x] -> str x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")" + | [_,x] -> str x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -174,7 +174,7 @@ end) = struct tag_type (str "Set") | GType u -> (match u with - | Some u -> str u + | Some (_,u) -> str u | None -> tag_type (str "Type")) let pr_universe_instance l = diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 71dcd15cc..00c276bdb 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -166,6 +166,8 @@ module Make (* This should not happen because of the grammar *) | IntValue (Some n) -> spc() ++ int n | StringValue s -> spc() ++ str s + | StringOptValue None -> mt() + | StringOptValue (Some s) -> spc() ++ str s | BoolValue b -> mt() in pr_printoption a None ++ pr_opt_value b @@ -354,6 +356,7 @@ module Make | l -> prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l + (* prlist_with_sep pr_semicolon (pr_params pr_c) *) @@ -772,11 +775,12 @@ module Make return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) | VernacAssumption (stre,_,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in - return ( - hov 2 - (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_lconstr_expr l) - ) + let pr_params (c, (xl, t)) = + hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++ + (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) + in + let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in + return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions)) | VernacInductive (p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 4aa3c3bfd..b1fba132d 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -117,7 +117,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit (** {6 ... } *) (** [set_used_variables l] declares that section variables [l] will be used in the proof *) -val set_used_variables : Id.t list -> Context.section_context +val set_used_variables : + Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list val get_used_variables : unit -> Context.section_context option (** {6 ... } *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index b5e25cc7c..96c80f263 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -253,17 +253,43 @@ let start_dependent_proof id str goals terminator = let get_used_variables () = (cur_pstate ()).section_vars +let proof_using_auto_clear = ref true +let _ = Goptions.declare_bool_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "Proof using Clear Unused"; + Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; + Goptions.optread = (fun () -> !proof_using_auto_clear); + Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } + let set_used_variables l = let env = Global.env () in let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in + let ctx_set = + List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in + let vars_of = Environ.global_vars_set in + let aux env entry (ctx, all_safe, to_clear as orig) = + match entry with + | (x,None,_) -> + if Id.Set.mem x all_safe then orig + else (ctx, all_safe, (Loc.ghost,x)::to_clear) + | (x,Some bo, ty) as decl -> + if Id.Set.mem x all_safe then orig else + let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in + if Id.Set.subset vars all_safe + then (decl :: ctx, Id.Set.add x all_safe, to_clear) + else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in + let ctx, _, to_clear = + Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in + let to_clear = if !proof_using_auto_clear then to_clear else [] in match !pstates with | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then Errors.error "Used section variables can be declared only once"; pstates := { p with section_vars = Some ctx} :: rest; - ctx + ctx, to_clear let get_open_goals () = let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in @@ -342,10 +368,6 @@ type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.ev let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin - if Proof.is_complete proof then begin - msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++ - str" is complete, no need to end it with Admitted"); - end; let proofs = Proof.partial_proof proof in let _,_,_,_, evd = Proof.proof proof in let eff = Evd.eval_side_effects evd in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 995e90efc..a11c7b4e0 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -132,8 +132,10 @@ val set_interp_tac : -> unit (** Sets the section variables assumed by the proof, returns its closure - * (w.r.t. type dependencies *) -val set_used_variables : Names.Id.t list -> Context.section_context + * (w.r.t. type dependencies and let-ins covered by it) + a list of + * ids to be cleared *) +val set_used_variables : + Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list val get_used_variables : unit -> Context.section_context option (**********************************************************) diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index f66e96571..7eed1cb31 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -11,20 +11,15 @@ open Environ open Util open Vernacexpr -let to_string = function - | SsAll -> "All" - | SsType -> "Type" - | SsExpr(SsSet l)-> String.concat " " (List.map Id.to_string (List.map snd l)) - | SsExpr e -> - let rec aux = function - | SsSet [] -> "( )" - | SsSet [_,x] -> Id.to_string x - | SsSet l -> - "(" ^ String.concat " " (List.map Id.to_string (List.map snd l)) ^ ")" - | SsCompl e -> "-" ^ aux e^"" - | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" - | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" - in aux e +let to_string e = + let rec aux = function + | SsEmpty -> "()" + | SsSingl (_,id) -> "("^Id.to_string id^")" + | SsCompl e -> "-" ^ aux e^"" + | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" + | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" + | SsFwdClose e -> "("^aux e^")*" + in aux e let known_names = Summary.ref [] ~name:"proofusing-nameset" @@ -36,30 +31,48 @@ let in_nameset = discharge_function = (fun _ -> None) } +let rec close_fwd e s = + let s' = + List.fold_left (fun s (id,b,ty) -> + let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in + let vty = global_vars_set e ty in + let vbty = Id.Set.union vb vty in + if Id.Set.exists (fun v -> Id.Set.mem v s) vbty + then Id.Set.add id (Id.Set.union s vbty) else s) + s (named_context e) + in + if Id.Set.equal s s' then s else close_fwd e s' +;; + let rec process_expr env e ty = - match e with - | SsAll -> - List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty - | SsExpr e -> - let rec aux = function - | SsSet l -> set_of_list env (List.map snd l) - | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) - | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) - | SsCompl e -> Id.Set.diff (full_set env) (aux e) - in - aux e - | SsType -> - List.fold_left (fun acc ty -> + let rec aux = function + | SsEmpty -> Id.Set.empty + | SsSingl (_,id) -> set_of_id env ty id + | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) + | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) + | SsCompl e -> Id.Set.diff (full_set env) (aux e) + | SsFwdClose e -> close_fwd env (aux e) + in + aux e + +and set_of_id env ty id = + if Id.to_string id = "Type" then + List.fold_left (fun acc ty -> Id.Set.union (global_vars_set env ty) acc) Id.Set.empty ty -and set_of_list env = function - | [x] when CList.mem_assoc_f Id.equal x !known_names -> - process_expr env (CList.assoc_f Id.equal x !known_names) [] - | l -> List.fold_right Id.Set.add l Id.Set.empty -and full_set env = set_of_list env (List.map pi1 (named_context env)) + else if Id.to_string id = "All" then + List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty + else if CList.mem_assoc_f Id.equal id !known_names then + process_expr env (CList.assoc_f Id.equal id !known_names) [] + else Id.Set.singleton id + +and full_set env = + List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty let process_expr env e ty = - let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in + let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in + let v_ty = process_expr env ty_expr ty in + let s = Id.Set.union v_ty (process_expr env e ty) in Id.Set.elements s let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) @@ -77,62 +90,49 @@ let minimize_hyps env ids = in aux ids -let minimize_unused_hyps env ids = - let all_ids = List.map pi1 (named_context env) in - let deps_of = - let cache = - List.map (fun id -> id,really_needed env (Id.Set.singleton id)) all_ids in - fun id -> List.assoc id cache in - let inv_dep_of = - let cache_sum cache id stuff = - try Id.Map.add id (Id.Set.add stuff (Id.Map.find id cache)) cache - with Not_found -> Id.Map.add id (Id.Set.singleton stuff) cache in - let cache = - List.fold_left (fun cache id -> - Id.Set.fold (fun d cache -> cache_sum cache d id) - (Id.Set.remove id (deps_of id)) cache) - Id.Map.empty all_ids in - fun id -> try Id.Map.find id cache with Not_found -> Id.Set.empty in - let rec aux s = - let s' = - Id.Set.fold (fun id s -> - if Id.Set.subset (inv_dep_of id) s then Id.Set.diff s (inv_dep_of id) - else s) - s s in - if Id.Set.equal s s' then s else aux s' in - aux ids - -let suggest_Proof_using kn env vars ids_typ context_ids = +let remove_ids_and_lets env s ids = + let not_ids id = not (Id.Set.mem id ids) in + let no_body id = named_body id env = None in + let deps id = really_needed env (Id.Set.singleton id) in + (Id.Set.filter (fun id -> + not_ids id && + (no_body id || + Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s) + +let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let used = S.union vars ids_typ in - let needed = minimize_hyps env used in - let all_needed = really_needed env needed in - let all = List.fold_right S.add context_ids S.empty in - let unneeded = minimize_unused_hyps env (S.diff all needed) in - let pr_set s = + let print x = prerr_endline (string_of_ppcmds x) in + let pr_set parens s = let wrap ppcmds = - if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All")) - then str "(" ++ ppcmds ++ str ")" + if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" else ppcmds in wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in + let used = S.union vars ids_typ in + let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in + let all_needed = really_needed env needed in + let all = List.fold_right S.add context_ids S.empty in + let fwd_typ = close_fwd env ids_typ in if !Flags.debug then begin - prerr_endline (string_of_ppcmds (str "All " ++ pr_set all)); - prerr_endline (string_of_ppcmds (str "Type" ++ pr_set ids_typ)); - prerr_endline (string_of_ppcmds (str "needed " ++ pr_set needed)); - prerr_endline (string_of_ppcmds (str "unneeded " ++ pr_set unneeded)); + print (str "All " ++ pr_set false all); + print (str "Type " ++ pr_set false ids_typ); + print (str "needed " ++ pr_set false needed); + print (str "all_needed " ++ pr_set false all_needed); + print (str "Type* " ++ pr_set false fwd_typ); end; + let valid_exprs = ref [] in + let valid e = valid_exprs := e :: !valid_exprs in + if S.is_empty needed then valid (str "Type"); + if S.equal all_needed fwd_typ then valid (str "Type*"); + if S.equal all all_needed then valid(str "All"); + valid (pr_set false needed); msg_info ( - str"The proof of "++ - Names.Constant.print kn ++ spc() ++ str "should start with:"++spc()++ - str"Proof using " ++ - if S.is_empty needed then str "." - else if S.subset needed ids_typ then str "Type." - else if S.equal all all_needed then str "All." - else - let s1 = string_of_ppcmds (str "-" ++ pr_set unneeded ++ str".") in - let s2 = string_of_ppcmds (pr_set needed ++ str".") in - if String.length s1 < String.length s2 then str s1 else str s2) + str"The proof of "++ str name ++ spc() ++ + str "should start with one of the following commands:"++spc()++ + v 0 ( + prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs)); + string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) +;; let value = ref false @@ -146,13 +146,13 @@ let _ = Goptions.optwrite = (fun b -> value := b; if b then Term_typing.set_suggest_proof_using suggest_Proof_using - else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> ()) + else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "") ) } -let value = ref "_unset_" +let value = ref None let _ = - Goptions.declare_string_option + Goptions.declare_stringopt_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = "default value for Proof using"; @@ -161,6 +161,4 @@ let _ = Goptions.optwrite = (fun b -> value := b;) } -let get_default_proof_using () = - if !value = "_unset_" then None - else Some !value +let get_default_proof_using () = !value diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli index fb3497f10..dcf8a0fcd 100644 --- a/proofs/proof_using.mli +++ b/proofs/proof_using.mli @@ -6,21 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(* [minimize_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true] - * and [keep_hyps e s1] is equal to [keep_hyps e s2]. Inefficient. *) -val minimize_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t - -(* [minimize_unused_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true] - * and s.t. calling [clear s1] would do the same as [clear s2]. Inefficient. *) -val minimize_unused_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t - val process_expr : - Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list -> + Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list -> Names.Id.t list -val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit +val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit -val to_string : Vernacexpr.section_subset_descr -> string +val to_string : Vernacexpr.section_subset_expr -> string val get_default_proof_using : unit -> string option diff --git a/stm/spawned.ml b/stm/spawned.ml index a8372195d..66fe07dbc 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -11,7 +11,7 @@ open Spawn let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s let prerr_endline s = if !Flags.debug then begin pr_err s end else () -type chandescr = AnonPipe | Socket of string * int +type chandescr = AnonPipe | Socket of string * int * int let handshake cin cout = try @@ -26,18 +26,19 @@ let handshake cin cout = | End_of_file -> pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") -let open_bin_connection h p = +let open_bin_connection h pr pw = let open Unix in - let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in + let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in + let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) in set_binary_mode_in cin true; set_binary_mode_out cout true; let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in cin, cout -let controller h p = +let controller h pr pw = prerr_endline "starting controller thread"; let main () = - let ic, oc = open_bin_connection h p in + let ic, oc = open_bin_connection h pr pw in let rec loop () = try match CThread.thread_friendly_input_value ic with @@ -61,8 +62,8 @@ let init_channels () = if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice"); let () = match !main_channel with | None -> () - | Some (Socket(mh,mp)) -> - channels := Some (open_bin_connection mh mp); + | Some (Socket(mh,mpr,mpw)) -> + channels := Some (open_bin_connection mh mpr mpw); | Some AnonPipe -> let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in @@ -74,8 +75,8 @@ let init_channels () = in match !control_channel with | None -> () - | Some (Socket (ch, cp)) -> - controller ch cp + | Some (Socket (ch, cpr, cpw)) -> + controller ch cpr cpw | Some AnonPipe -> Errors.anomaly (Pp.str "control channel cannot be a pipe") diff --git a/stm/spawned.mli b/stm/spawned.mli index d9e7baff3..d0183e081 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -8,7 +8,7 @@ (* To link this file, threads are needed *) -type chandescr = AnonPipe | Socket of string * int +type chandescr = AnonPipe | Socket of string * int * int (* Argument parsing should set these *) val main_channel : chandescr option ref diff --git a/stm/stm.ml b/stm/stm.ml index f178c3ae4..c7836d118 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -888,9 +888,16 @@ let set_compilation_hints file = hints := Aux_file.load_aux_file_for file let get_hint_ctx loc = let s = Aux_file.get !hints loc "context_used" in - let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in - let ids = List.map (fun id -> Loc.ghost, id) ids in - SsExpr (SsSet ids) + match Str.split (Str.regexp ";") s with + | ids :: _ -> + let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in + let ids = List.map (fun id -> Loc.ghost, id) ids in + begin match ids with + | [] -> SsEmpty + | x :: xs -> + List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs + end + | _ -> raise Not_found let get_hint_bp_time proof_name = try float_of_string (Aux_file.get !hints Loc.ghost proof_name) @@ -1577,7 +1584,8 @@ end = struct (* {{{ *) vernac_interp r_for { r_what with verbose = true }; feedback ~state_id:r_for Feedback.Processed with e when Errors.noncritical e -> - let msg = string_of_ppcmds (print e) in + let e = Errors.push e in + let msg = string_of_ppcmds (iprint e) in feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg)) let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) @@ -2341,7 +2349,8 @@ let edit_at id = VCS.delete_cluster_of id; VCS.gc (); VCS.print (); - Reach.known_state ~cache:(interactive ()) id; + if not !Flags.async_proofs_full then + Reach.known_state ~cache:(interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try diff --git a/stm/stm.mli b/stm/stm.mli index 1d926e998..4bad7f0a6 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -35,7 +35,9 @@ val query : new document tip, the document between [id] and [fo.stop] has been dropped. The portion between [fo.stop] and [fo.tip] has been kept. [fo.start] is just to tell the gui where the editing zone starts, in case it wants to - graphically denote it. All subsequent [add] happen on top of [id]. *) + graphically denote it. All subsequent [add] happen on top of [id]. + If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is. +*) type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] @@ -49,11 +51,11 @@ val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) val join : unit -> unit -(* Saves on the dist a .vio corresponding to the current status: - - if the worker prool is empty, all tasks are saved +(* Saves on the disk a .vio corresponding to the current status: + - if the worker pool is empty, all tasks are saved - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one - of the completed tasks is a failuere) *) + of the completed tasks is a failure) *) val snapshot_vio : DirPath.t -> string -> unit (* Empties the task queue, can be used only if the worker pool is empty (E.g. diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index fb41bb7be..b91208041 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -575,10 +575,11 @@ let rec tmpp v loc = end | VernacExactProof _ as x -> xmlTODO loc x | VernacAssumption ((l, a), _, sbwcl) -> + let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in let many = - List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in + List.length (List.flatten (List.map fst binders)) > 1 in let exprs = - List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in + List.flatten (List.map pp_simple_binder binders) in let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8aa2a5917..a898c687b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -141,7 +141,7 @@ let rec classify_vernac e = else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in VtSideff ids, VtLater | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater | VernacInductive (_,_,l) -> diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index 4cd7c39e8..e6a50449d 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index b57b0a0f0..f8113e4c7 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo]. (I think this worked in HoTT/coq, too.) Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A]. (The issue is tricker when IsHProp uses [A] elsewhere, as in: diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v index 0e236c217..b8bb8bce0 100644 --- a/test-suite/bugs/closed/3386.v +++ b/test-suite/bugs/closed/3386.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Universe Polymorphism. Set Printing Universes. Record Cat := { Obj :> Type }. diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v index ae212caa5..cb435e786 100644 --- a/test-suite/bugs/closed/3387.v +++ b/test-suite/bugs/closed/3387.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Universe Polymorphism. Set Printing Universes. Record Cat := { Obj :> Type }. diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v index 50645090f..da12b6868 100644 --- a/test-suite/bugs/closed/3559.v +++ b/test-suite/bugs/closed/3559.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* File reduced by coq-bug-finder from original input, then from 8657 lines to 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines, then from 51 lines to 37 lines, then from 43 lines to 30 lines *) diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v index b2aa8c3cd..e2d797698 100644 --- a/test-suite/bugs/closed/3566.v +++ b/test-suite/bugs/closed/3566.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Notation idmap := (fun x => x). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. Arguments idpath {A a} , [A] a. diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v index a5b0e9347..e69ec1097 100644 --- a/test-suite/bugs/closed/3666.v +++ b/test-suite/bugs/closed/3666.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *) (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *) diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index 4069e3807..df9f5f476 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Printing Universes. Set Universe Polymorphism. Definition foo (a := Type) (b := Type) (c := Type) := Type. diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v index b9b2dd6b3..e203528fc 100644 --- a/test-suite/bugs/closed/3777.v +++ b/test-suite/bugs/closed/3777.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Module WithoutPoly. Unset Universe Polymorphism. Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B. diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v index eb0d206c5..2b44e225e 100644 --- a/test-suite/bugs/closed/3779.v +++ b/test-suite/bugs/closed/3779.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Universe Polymorphism. Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }. Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T. diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v index 6e19ddf8d..a5c84e685 100644 --- a/test-suite/bugs/closed/3808.v +++ b/test-suite/bugs/closed/3808.v @@ -1,2 +1,3 @@ +Unset Strict Universe Declaration. Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i}) := foo : Foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v index 8da4f7362..30261ed26 100644 --- a/test-suite/bugs/closed/3821.v +++ b/test-suite/bugs/closed/3821.v @@ -1,2 +1,3 @@ +Unset Strict Universe Declaration. Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := . diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 0ccc92067..5013bc6ac 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. Set Universe Polymorphism. Notation Type0 := Set. diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v new file mode 100644 index 000000000..21b03ce54 --- /dev/null +++ b/test-suite/bugs/closed/4069.v @@ -0,0 +1,51 @@ + +Lemma test1 : +forall (v : nat) (f g : nat -> nat), +f v = g v. +intros. f_equal. +(* +Goal in v8.5: f v = g v +Goal in v8.4: v = v -> f v = g v +Expected: f = g +*) +Admitted. + +Lemma test2 : +forall (v u : nat) (f g : nat -> nat), +f v = g u. +intros. f_equal. +(* +In both v8.4 And v8.5 +Goal 1: v = u -> f v = g u +Goal 2: v = u + +Expected Goal 1: f = g +Expected Goal 2: v = u +*) +Admitted. + +Lemma test3 : +forall (v : nat) (u : list nat) (f : nat -> nat) (g : list nat -> nat), +f v = g u. +intros. f_equal. +(* +In both v8.4 And v8.5, the goal is unchanged. +*) +Admitted. + +Require Import List. +Lemma foo n (l k : list nat) : k ++ skipn n l = skipn n l. +Proof. f_equal. +(* + 8.4: leaves the goal unchanged, i.e. k ++ skipn n l = skipn n l + 8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l + and skipn n l = l +*) +Require Import List. +Fixpoint replicate {A} (n : nat) (x : A) : list A := + match n with 0 => nil | S n => x :: replicate n x end. +Lemma bar {A} n m (x : A) : + skipn n (replicate m x) = replicate (m - n) x -> + skipn n (replicate m x) = replicate (m - n) x. +Proof. intros. f_equal. +(* 8.5: one goal, n = m - n *) diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index c6cb9c35e..e4d76732a 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *) diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index 5f8c411ca..d34a2b8b1 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* -*- coq-prog-args: ("-emacs" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *) (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v new file mode 100644 index 000000000..aa2b189b6 --- /dev/null +++ b/test-suite/bugs/closed/4161.v @@ -0,0 +1,27 @@ + + (* Inductive t : Type -> Type := *) + (* | Just : forall (A : Type), t A -> t A. *) + + (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *) + (* match x in t A return t (A + unit) with *) + (* | Just T x => @test T x *) + (* end. *) + + + Definition Type1 := Type. +Definition Type2 := Type. +Definition cast (x:Type2) := x:Type1. +Axiom f: Type2 -> Prop. +Definition A := + let T := fun A:Type1 => _ in + fun A':Type2 => + eq_refl : T A' = f A' :> Prop. +(* Type2 <= Type1... f A -> Type1 <= Type2 *) + +Inductive t : Type -> Type := + | Just : forall (A : Type), t A -> t A. + +Fixpoint test {A : Type} (x : t A) : t (A + unit) := + match x in t A with + | Just B x => @test B x + end.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v index e139c5b6c..0623cf5b8 100644 --- a/test-suite/bugs/closed/4287.v +++ b/test-suite/bugs/closed/4287.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Universe b. diff --git a/test-suite/bugs/closed/4299.v b/test-suite/bugs/closed/4299.v new file mode 100644 index 000000000..955c3017d --- /dev/null +++ b/test-suite/bugs/closed/4299.v @@ -0,0 +1,12 @@ +Unset Strict Universe Declaration. +Set Universe Polymorphism. + +Module Type Foo. + Definition U := Type : Type. + Parameter eq : Type = U. +End Foo. + +Module M : Foo with Definition U := Type : Type. + Definition U := let X := Type in Type. + Definition eq : Type = U := eq_refl. +Fail End M.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v index 3b00efb21..b4e17c223 100644 --- a/test-suite/bugs/closed/4301.v +++ b/test-suite/bugs/closed/4301.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Universe Polymorphism. Module Type Foo. diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v index 0b8bb2353..844ff8756 100644 --- a/test-suite/bugs/closed/HoTT_coq_007.v +++ b/test-suite/bugs/closed/HoTT_coq_007.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. Module Comment1. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v index 4c3e078a5..7a84531a7 100644 --- a/test-suite/bugs/closed/HoTT_coq_036.v +++ b/test-suite/bugs/closed/HoTT_coq_036.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Module Version1. Set Implicit Arguments. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index b7db22a69..90d1d1830 100644 --- a/test-suite/bugs/closed/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *) diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v index f382dac97..4f8868d53 100644 --- a/test-suite/bugs/closed/HoTT_coq_093.v +++ b/test-suite/bugs/closed/HoTT_coq_093.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *) Set Printing All. Set Printing Implicit. diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v index 9b3f94d91..a717bbe73 100644 --- a/test-suite/bugs/opened/3754.v +++ b/test-suite/bugs/opened/3754.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *) (* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1 diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index 059462fac..f9154ef57 100644 --- a/test-suite/success/namedunivs.v +++ b/test-suite/success/namedunivs.v @@ -4,6 +4,8 @@ (* Fail exact H. *) (* Section . *) +Unset Strict Universe Declaration. + Section lift_strict. Polymorphic Definition liftlt := let t := Type@{i} : Type@{k} in diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 957612ef1..d6bbfe29a 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -1,3 +1,5 @@ +Unset Strict Universe Declaration. + Module withoutpoly. Inductive empty :=. diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index 61e73f858..c83f45e2a 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -117,5 +117,81 @@ End T1. Check (bla 7 : 2 = 8). +Section A. +Variable a : nat. +Variable b : nat. +Variable c : nat. +Variable H1 : a = 3. +Variable H2 : a = 3 -> b = 7. +Variable H3 : c = 3. + +Lemma foo : a = a. +Proof using Type*. +pose H1 as e1. +pose H2 as e2. +reflexivity. +Qed. + +Lemma bar : a = 3 -> b = 7. +Proof using b*. +exact H2. +Qed. + +Lemma baz : c=3. +Proof using c*. +exact H3. +Qed. + +Lemma baz2 : c=3. +Proof using c* a. +exact H3. +Qed. + +End A. + +Check (foo 3 7 (refl_equal 3) + (fun _ => refl_equal 7)). +Check (bar 3 7 (refl_equal 3) + (fun _ => refl_equal 7)). +Check (baz2 99 3 (refl_equal 3)). +Check (baz 3 (refl_equal 3)). + +Section Let. + +Variables a b : nat. +Let pa : a = a. Proof. reflexivity. Qed. +Unset Default Proof Using. +Set Suggest Proof Using. +Lemma test_let : a = a. +Proof using a. +exact pa. +Qed. + +Let ppa : pa = pa. Proof. reflexivity. Qed. + +Lemma test_let2 : pa = pa. +Proof using Type. +exact ppa. +Qed. + +End Let. + +Check (test_let 3). + +Section Clear. + +Variable a: nat. +Hypotheses H : a = 4. + +Set Proof Using Clear Unused. + +Lemma test_clear : a = a. +Proof using a. +Fail rewrite H. +trivial. +Qed. + +End Clear. + diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v new file mode 100644 index 000000000..db2bbb0dc --- /dev/null +++ b/test-suite/success/record_syntax.v @@ -0,0 +1,47 @@ +Module A. + +Record Foo := { foo : unit; bar : unit }. + +Definition foo_ := {| + foo := tt; + bar := tt +|}. + +Definition foo0 (p : Foo) := match p with {| |} => tt end. +Definition foo1 (p : Foo) := match p with {| foo := f |} => f end. +Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end. +Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end. +Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end. + +End A. + +Module B. + +Record Foo := { }. + +End B. + +Module C. + +Record Foo := { foo : unit; bar : unit; }. + +Definition foo_ := {| + foo := tt; + bar := tt; +|}. + +End C. + +Module D. + +Record Foo := { foo : unit }. +Definition foo_ := {| foo := tt |}. + +End D. + +Module E. + +Record Foo := { foo : unit; }. +Definition foo_ := {| foo := tt; |}. + +End E. diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v new file mode 100644 index 000000000..31d264f64 --- /dev/null +++ b/test-suite/success/univnames.v @@ -0,0 +1,26 @@ +Set Universe Polymorphism. + +Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A. + +Set Printing Universes. + +Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A. + +Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type. + +Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type. + +Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type. + +Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type. + +Definition nothing (A : Type) := A. + +Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. + +Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. + + +Universe g. + +Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 9d3952e64..fdedbf672 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -266,8 +266,10 @@ Section GenericInstances. transitivity (y x0)... Qed. + Unset Strict Universe Declaration. + (** The complement of a crelation conserves its proper elements. *) - Program Definition complement_proper + Program Definition complement_proper (A : Type@{k}) (RA : crelation A) `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _. @@ -279,7 +281,6 @@ Section GenericInstances. Qed. (** The [flip] too, actually the [flip] instance is a bit more general. *) - Program Definition flip_proper `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : Proper (RB ==> RA ==> RC) (flip f) := _. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 67e9a20cc..892305b49 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -32,10 +32,3 @@ Require List. Export List.ListNotations. Require Import Bvector. - -(** Treating n-ary exists *) - -Tactic Notation "exists" constr(x) := exists x. -Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y. -Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. -Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. diff --git a/toplevel/command.ml b/toplevel/command.ml index b65ff73fe..e54a82c19 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -251,7 +251,7 @@ let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl = in List.rev refs, status -let do_assumptions (_, poly, _ as kind) nl l = +let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let env = Global.env () in let evdref = ref (Evd.from_env env) in let l = @@ -284,6 +284,44 @@ let do_assumptions (_, poly, _ as kind) nl l = in (subst'@subst, status' && status)) ([],true) l) +let do_assumptions_bound_univs coe kind nl id pl c = + let env = Global.env () in + let ctx = Evd.make_evar_universe_context env pl in + let evdref = ref (Evd.from_ctx ctx) in + let ty, impls = interp_type_evars_impls env evdref c in + let nf, subst = Evarutil.e_nf_evars_and_universes evdref in + let ty = nf ty in + let vars = Universes.universes_of_constr ty in + let evd = Evd.restrict_universe_context !evdref vars in + let uctx = Evd.universe_context ?names:pl evd in + let uctx = Univ.ContextSet.of_context uctx in + let (_, _, st) = declare_assumption coe kind (ty, uctx) impls false nl id in + st + +let do_assumptions kind nl l = match l with +| [coe, ([id, Some pl], c)] -> + let () = match kind with + | (Discharge, _, _) when Lib.sections_are_opened () -> + let loc = fst id in + let msg = Pp.str "Section variables cannot be polymorphic." in + user_err_loc (loc, "", msg) + | _ -> () + in + do_assumptions_bound_univs coe kind nl id (Some pl) c +| _ -> + let map (coe, (idl, c)) = + let map (id, univs) = match univs with + | None -> id + | Some _ -> + let loc = fst id in + let msg = Pp.str "Assumptions with bound universes can only be defined once at a time." in + user_err_loc (loc, "", msg) + in + (coe, (List.map map idl, c)) + in + let l = List.map map l in + do_assumptions_unbound_univs kind nl l + (* 3a| Elimination schemes for mutual inductive definitions *) (* 3b| Mutual inductive definitions *) @@ -500,12 +538,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in - let evdref = ref Evd.(from_env env0) in + let pl = (List.hd indl).ind_univs in + let ctx = Evd.make_evar_universe_context env0 pl in + let evdref = ref Evd.(from_ctx ctx) in let _, ((env_params, ctx_params), userimpls) = interp_context_evars env0 evdref paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in - let pl = (List.hd indl).ind_univs in (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in diff --git a/toplevel/command.mli b/toplevel/command.mli index f4d43ec53..b1e1d7d06 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -57,7 +57,7 @@ val declare_assumption : coercion_flag -> assumption_kind -> global_reference * Univ.Instance.t * bool val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> simple_binder with_coercion list -> bool + Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool (* val declare_assumptions : variable Loc.located list -> *) (* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 076db5e11..d41ecebe0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -359,7 +359,8 @@ let get_int opt n = let get_host_port opt s = match CString.split ':' s with - | [host; port] -> Some (Spawned.Socket(host, int_of_string port)) + | [host; portr; portw] -> + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) | ["stdfds"] -> Some Spawned.AnonPipe | _ -> prerr_endline ("Error: host:port or stdfds expected after option "^opt); diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index d2bd2c07b..836de042b 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -798,7 +798,7 @@ let solve_by_tac name evi t poly ctx = let entry = Term_typing.handle_entry_side_effects env entry in let body, eff = Future.force entry.Entries.const_entry_body in assert(Declareops.side_effects_is_empty eff); - let ctx' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in + let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx' diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 229f3acfd..d0e231b26 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -515,7 +515,7 @@ let vernac_assumption locality poly (local, kind) l nl = let kind = local, poly, kind in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then - List.iter (fun lid -> + List.iter (fun (lid, _) -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; let status = do_assumptions kind nl l in @@ -874,18 +874,7 @@ let vernac_set_used_variables e = errorlabstrm "vernac_set_used_variables" (str "Unknown variable: " ++ pr_id id)) l; - let closure_l = List.map pi1 (set_used_variables l) in - let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in - let vars_of = Environ.global_vars_set in - let aux env entry (all_safe,rest as orig) = - match entry with - | (x,None,_) -> - if Id.Set.mem x all_safe then orig else (all_safe, (Loc.ghost,x)::rest) - | (x,Some bo, ty) -> - let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in - if Id.Set.subset vars all_safe then (Id.Set.add x all_safe, rest) - else (all_safe, (Loc.ghost,x) :: rest) in - let _,to_clear = Environ.fold_named_context aux env ~init:(closure_l,[]) in + let _, to_clear = set_used_variables l in vernac_solve SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false @@ -1497,6 +1486,8 @@ let vernac_set_opacity locality (v,l) = let vernac_set_option locality key = function | StringValue s -> set_string_option_value_gen locality key s + | StringOptValue (Some s) -> set_string_option_value_gen locality key s + | StringOptValue None -> unset_option_value_gen locality key | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b @@ -1855,8 +1846,9 @@ let vernac_load interp fname = (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility *) -let interp ?proof locality poly c = + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let interp ?proof ~loc locality poly c = prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* Done later in this file *) @@ -2000,10 +1992,16 @@ let interp ?proof locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> () - | VernacProof (Some tac, None) -> vernac_set_end_tac tac - | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (None, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no" + | VernacProof (Some tac, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no"; + vernac_set_end_tac tac + | VernacProof (None, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes"; + vernac_set_used_variables l | VernacProof (Some tac, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes"; vernac_set_end_tac tac; vernac_set_used_variables l | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) @@ -2155,8 +2153,9 @@ let interp ?(verbosely=true) ?proof (loc,c) = Obligations.set_program_mode isprogcmd; try vernac_timeout begin fun () -> - if verbosely then Flags.verbosely (interp ?proof locality poly) c - else Flags.silently (interp ?proof locality poly) c; + if verbosely + then Flags.verbosely (interp ?proof ~loc locality poly) c + else Flags.silently (interp ?proof ~loc locality poly) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode end |