diff options
Diffstat (limited to 'vernac')
32 files changed, 221 insertions, 145 deletions
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 7e13f8f284..0e2b0c80e8 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -30,4 +30,4 @@ val traverse : {!traverse} also applies. *) val assumptions : ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> - global_reference -> constr -> types ContextObjectMap.t + GlobRef.t -> constr -> types ContextObjectMap.t diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 1a6b4dcdb2..2a41a50ddf 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -54,20 +54,20 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of global_reference +exception ParameterWithoutEquality of GlobRef.t exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive -let constr_of_global g = lazy (Universes.constr_of_global g) +let constr_of_global g = lazy (UnivGen.constr_of_global g) (* Some pre declaration of constant we are going to use *) let bb = constr_of_global Coqlib.glob_bool -let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop +let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop let andb_true_intro = fun _ -> - Universes.constr_of_global + UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_true_intro let tt = constr_of_global Coqlib.glob_true @@ -76,9 +76,9 @@ let ff = constr_of_global Coqlib.glob_false let eq = constr_of_global Coqlib.glob_eq -let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ()) +let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ()) -let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb +let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = induction false None c None None @@ -635,7 +635,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | App (c,ca) -> ( match EConstr.kind sigma c with | Ind (indeq, u) -> - if eq_gr (IndRef indeq) Coqlib.glob_eq + if GlobRef.equal (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN (do_replace_bl mode bl_scheme_key ind @@ -863,7 +863,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) ) ) ) diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 5cc783df74..11f26c7c36 100644 --- a/vernac/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli @@ -23,7 +23,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of Globnames.global_reference +exception ParameterWithoutEquality of GlobRef.t exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive diff --git a/vernac/class.ml b/vernac/class.ml index f0b01061bf..06e1694f91 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -37,7 +37,7 @@ type coercion_error_kind = | ForbiddenSourceClass of cl_typ | NoTarget | WrongTarget of cl_typ * cl_typ - | NotAClass of global_reference + | NotAClass of GlobRef.t exception CoercionError of coercion_error_kind diff --git a/vernac/class.mli b/vernac/class.mli index 33d31fe1f8..f7e837f3bb 100644 --- a/vernac/class.mli +++ b/vernac/class.mli @@ -10,19 +10,18 @@ open Names open Classops -open Globnames (** Classes and coercions. *) (** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion from [src] to [tg] *) -val try_add_new_coercion_with_target : global_reference -> local:bool -> +val try_add_new_coercion_with_target : GlobRef.t -> local:bool -> Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit (** [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) -val try_add_new_coercion : global_reference -> local:bool -> +val try_add_new_coercion : GlobRef.t -> local:bool -> Decl_kinds.polymorphic -> unit (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a @@ -34,7 +33,7 @@ val try_add_new_coercion_subclass : cl_typ -> local:bool -> (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) -val try_add_new_coercion_with_source : global_reference -> local:bool -> +val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> Decl_kinds.polymorphic -> source:cl_typ -> unit (** [try_add_new_identity_coercion id s src tg] enriches the @@ -47,4 +46,4 @@ val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook -val class_of_global : global_reference -> cl_typ +val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/classes.ml b/vernac/classes.ml index 3c133f3175..61ce5d6c4c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -51,7 +51,6 @@ let _ = | IsGlobal gr -> Hints.IsGlobRef gr in let info = - let open Vernacexpr in { info with hint_pattern = Option.map (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env()))) @@ -196,7 +195,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in Pretyping.check_evars env Evd.empty sigma termtype; let univs = Evd.check_univ_decl ~poly sigma decl in let termtype = to_constr sigma termtype in @@ -289,7 +288,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in let sigma = Evarutil.nf_evar_map_undefined sigma in (* Beware of this step, it is required as to minimize universes. *) - let sigma, _nf = Evarutil.nf_evar_map_universes sigma in + let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) Pretyping.check_evars env Evd.empty sigma termtype; let termtype = to_constr sigma termtype in @@ -365,7 +364,7 @@ let context poly l = let sigma = Evd.from_env env in let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in (* Note, we must use the normalized evar from now on! *) - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env Evd.empty sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = @@ -424,13 +423,13 @@ let context poly l = let decl = (Discharge, poly, Definitional) in let nstatus = match b with | None -> - pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl - Vernacexpr.NoInline (CAst.make id)) + pi3 (ComAssumption.declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl + Declaremods.NoInline (CAst.make id)) | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in + let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/classes.mli b/vernac/classes.mli index 0342c840ee..27d3a4669d 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,15 +22,15 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a (** Instance declaration *) -val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit +val existing_instance : bool -> reference -> hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val declare_instance_constant : typeclass -> - Vernacexpr.hint_info_expr -> (** priority *) + hint_info_expr -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) - ?hook:(Globnames.global_reference -> unit) -> + ?hook:(GlobRef.t -> unit) -> Id.t -> (** name *) Univdecls.universe_decl -> bool -> (* polymorphic *) @@ -50,8 +50,8 @@ val new_instance : (bool * constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> - ?hook:(Globnames.global_reference -> unit) -> - Vernacexpr.hint_info_expr -> + ?hook:(GlobRef.t -> unit) -> + hint_info_expr -> Id.t (** Setting opacity *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 6a590758fd..722f21171f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -20,7 +20,6 @@ open Constrintern open Impargs open Decl_kinds open Pretyping -open Vernacexpr open Entries (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) @@ -66,7 +65,7 @@ match local with | Global | Local | Discharge -> let do_instance = should_axiom_into_instance local in let local = DeclareDef.get_locality ident ~kind:"axiom" local in - let inl = match nl with + let inl = let open Declaremods in match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i @@ -175,7 +174,7 @@ let do_assumptions kind nl l = let t = replace_vars subst t in let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u))) + (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u))) idl refs in subst'@subst, status' && status, next_uctx uctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 56e3243766..56932360a9 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -11,7 +11,6 @@ open Names open Constr open Entries -open Globnames open Vernacexpr open Constrexpr open Decl_kinds @@ -19,7 +18,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool + Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) @@ -31,6 +30,6 @@ val do_assumptions : locality * polymorphic * assumption_object_kind -> nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> types in_constant_universes_entry -> - Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t -> - global_reference * Univ.Instance.t * bool + UnivNames.universe_binders -> Impargs.manual_implicits -> + bool (** implicit *) -> Declaremods.inline -> variable CAst.t -> + GlobRef.t * Univ.Instance.t * bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9aa61ab460..863adb0d14 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -90,7 +90,7 @@ let interp_definition pl bl poly red_option c ctypopt = Note: in program mode some evars may remain. *) let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in - let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in + let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) @@ -118,7 +118,7 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1466fa243f..85c0699ea9 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -199,9 +199,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = try let sigma, h_term = fix_proto sigma in let app = mkApp (h_term, [|sort; t|]) in - let _evd = ref sigma in - let res = Typing.e_solve_evars env _evd app in - !_evd, res + Typing.solve_evars env sigma app with e when CErrors.noncritical e -> sigma, t in sigma, LocalAssum (id,fixprot) :: env' @@ -224,7 +222,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in - let sigma, _ = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in (* XXX: We still have evars here in Program *) let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 05c40dbdd7..629fcce5a7 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -29,7 +29,6 @@ open Indtypes open Pretyping open Evarutil open Indschemes -open Misctypes open Context.Rel.Declaration open Entries @@ -178,6 +177,72 @@ let is_flexible_sort evd u = | Some l -> Evd.is_flexible_level evd l | None -> false +(**********************************************************************) +(* Tools for template polymorphic inductive types *) + +(* Miscellaneous functions to remove or test local univ assumed to + occur only in the le constraints *) + +(* + Solve a system of universe constraint of the form + + u_s11, ..., u_s1p1, w1 <= u1 + ... + u_sn1, ..., u_snpn, wn <= un + +where + + - the ui (1 <= i <= n) are universe variables, + - the sjk select subsets of the ui for each equations, + - the wi are arbitrary complex universes that do not mention the ui. +*) + +let is_direct_sort_constraint s v = match s with + | Some u -> Univ.univ_level_mem u v + | None -> false + +let solve_constraints_system levels level_bounds = + let open Univ in + let levels = + Array.mapi (fun i o -> + match o with + | Some u -> + (match Universe.level u with + | Some u -> Some u + | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None) + | None -> None) + levels in + let v = Array.copy level_bounds in + let nind = Array.length v in + let clos = Array.map (fun _ -> Int.Set.empty) levels in + (* First compute the transitive closure of the levels dependencies *) + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then + clos.(i) <- Int.Set.add j clos.(i); + done; + done; + let rec closure () = + let continue = ref false in + Array.iteri (fun i deps -> + let deps' = + Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps + in + if Int.Set.equal deps deps' then () + else (clos.(i) <- deps'; continue := true)) + clos; + if !continue then closure () + else () + in + closure (); + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && Int.Set.mem j clos.(i) then + (v.(i) <- Universe.sup v.(i) level_bounds.(j)); + done; + done; + v + let inductive_levels env evd poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> @@ -206,8 +271,8 @@ let inductive_levels env evd poly arities inds = in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) - let levels' = Universes.solve_constraints_system (Array.of_list levels) - (Array.of_list cstrs_levels) (Array.of_list min_levels) + let levels' = solve_constraints_system (Array.of_list levels) + (Array.of_list cstrs_levels) in let evd, arities = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> @@ -304,14 +369,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in (* Compute renewed arities *) - let sigma, nf = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in - let sigma, nf' = nf_evars_and_universes sigma in - let arities = List.map nf' arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in + let arities = List.map nf arities in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let uctx = Evd.check_univ_decl ~poly sigma decl in List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; @@ -378,7 +445,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; - ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar; ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 8339357246..7ae8e8f716 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -37,7 +37,7 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val declare_mutual_inductive_with_eliminations : - mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> + mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> MutInd.t (** Exported for Funind *) @@ -64,4 +64,4 @@ val extract_mutual_inductive_declaration_components : val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> polymorphic -> private_flag -> Declarations.recursivity_kind -> - mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list + mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 745f1df1d8..f41e0fc443 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -190,9 +190,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in - let _evd = ref sigma in - let def = Typing.e_solve_evars env _evd def in - let sigma = !_evd in + let sigma, def = Typing.solve_evars env sigma def in let sigma = Evarutil.nf_evar_map sigma in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context sigma binders_rel in @@ -214,7 +212,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in - let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in + let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 010874e23c..c5e704a5e9 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -8,17 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Decl_kinds open Names +open Decl_kinds val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool val declare_definition : Id.t -> definition_kind -> - Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> - Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference + Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> + GlobRef.t Lemmas.declaration_hook -> GlobRef.t val declare_fix : ?opaque:bool -> definition_kind -> - Universes.universe_binders -> Entries.constant_universes_entry -> + UnivNames.universe_binders -> Entries.constant_universes_entry -> Id.t -> Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> - Globnames.global_reference + GlobRef.t diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index f9167f9691..f68dcae268 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -55,7 +55,7 @@ let process_vernac_interp_error exn = match fst exn with let msg = if !Constrextern.print_universes then str "." ++ spc() ++ - Univ.explain_universe_inconsistency Universes.pr_with_global_universes i + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i else mt() in wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") diff --git a/vernac/himsg.ml b/vernac/himsg.ml index acb461cacd..3c4fcf7145 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -197,7 +197,7 @@ let rec pr_disjunction pr = function let pr_puniverses f env (c,u) = f env c ++ (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" else mt()) let explain_elim_arity env sigma ind sorts c pj okinds = @@ -314,7 +314,7 @@ let explain_unification_error env sigma p1 p2 = function | UnifUnivInconsistency p -> if !Constrextern.print_universes then [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency Universes.pr_with_global_universes p] + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p] else [str "universe inconsistency"] | CannotSolveConstraint ((pb,env,t,u),e) -> @@ -886,7 +886,7 @@ let explain_not_match_error = function str"polymorphic universe instances do not match" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ - Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon | IncompatiblePolymorphism (env, t1, t2) -> str "conversion of polymorphic values generates additional constraints: " ++ quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++ diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 32885ab88a..2deca1e069 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -380,7 +380,7 @@ let do_mutual_induction_scheme lnamedepindsort = match inst with | None -> let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in - let u, ctx = Universes.fresh_instance_from ctx None in + let u, ctx = UnivGen.fresh_instance_from ctx None in let evd = Evd.from_ctx (UState.of_context_set ctx) in evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 30dd6ec74a..3c7ede3c99 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -34,7 +34,7 @@ open Impargs module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a +type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a let mk_hook hook = hook let call_hook fix_exn hook l c = try hook l c @@ -334,8 +334,8 @@ let universe_proof_terminator compute_guard hook = Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff = match opaque with - | Vernacexpr.Transparent -> false, true - | Vernacexpr.Opaque -> true, false + | Transparent -> false, true + | Opaque -> true, false in let proof = get_proof proof compute_guard (hook (Some (proof.Proof_global.universes))) is_opaque in @@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook = (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) evd thms in let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in - let evd, _nf = Evarutil.nf_evars_and_universes evd in + let evd = Evd.minimize_universes evd in (* XXX: This nf_evar is critical too!! We are normalizing twice if you look at the previous lines... *) let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index ad4c278e03..398f7d6d0a 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -13,10 +13,10 @@ open Decl_kinds type 'a declaration_hook val mk_hook : - (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook + (Decl_kinds.locality -> GlobRef.t -> 'a) -> 'a declaration_hook val call_hook : - Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a + Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> GlobRef.t -> 'a (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (EConstr.types -> unit) -> unit diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index feeca60753..76958b05fd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -738,12 +738,12 @@ let cache_one_syntax_extension se = let prec = se.synext_level in let onlyprint = se.synext_notgram.notgram_onlyprinting in try - let oldprec = Notation.level_of_notation ntn in + let oldprec = Notation.level_of_notation ~onlyprint ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; + Notation.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) @@ -1274,7 +1274,7 @@ exception NoSyntaxRule let recover_notation_syntax ntn = try - let prec = Notation.level_of_notation ntn in + let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in let pp_rule,_ = Notation.find_notation_printing_rule ntn in let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in let pa_rule = Notation.find_notation_parsing_rules ntn in diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 343b0925d9..d25dea1413 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -345,13 +345,6 @@ let load_ml_object mname ?path fname= let dir_ml_load m = ignore(dir_ml_load m) let add_known_module m = add_known_module m None -let load_ml_object_raw fname = dir_ml_load (file_of_name fname) -let load_ml_objects_raw_rex rex = - List.iter (fun (_,fp) -> - let name = file_of_name (Filename.basename fp) in - try dir_ml_load name - with e -> prerr_endline (Printexc.to_string e)) - (System.where_in_path_rex !coq_mlpath_copy rex) (* Summary of declared ML Modules *) @@ -396,8 +389,6 @@ let trigger_ml_object verb cache reinit ?path name = if cache then perform_cache_obj name end -let load_ml_object n m = ignore(load_ml_object n m) - let unfreeze_ml_modules x = reset_loaded_modules (); List.iter diff --git a/vernac/mltop.mli b/vernac/mltop.mli index da195f4fce..ed1f9a12d8 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -68,9 +68,6 @@ val add_coq_path : coq_path -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool -val load_ml_object : string -> string -> unit -val load_ml_object_raw : string -> unit -val load_ml_objects_raw_rex : Str.regexp -> unit (** {5 Initialization functions} *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 3f2792518b..3bf0ca0a87 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -259,7 +259,7 @@ let eterm_obligations env name evm fs ?status t ty = let tactics_module = ["Program";"Tactics"] let safe_init_constant md name () = Coqlib.check_required_library ("Coq"::md); - Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name) + UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name) let hide_obligation = safe_init_constant tactics_module "obligation" let pperror cmd = CErrors.user_err ~hdr:"Program" cmd @@ -472,7 +472,7 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in - let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) + let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None) (UState.subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in @@ -555,13 +555,13 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let univs = UState.const_univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - let kn = match gr with ConstRef kn -> kn | _ -> assert false in + let kn = match gr with GlobRef.ConstRef kn -> kn | _ -> assert false in Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; List.iter progmap_remove l; kn @@ -744,7 +744,7 @@ let all_programs () = type progress = | Remain of int | Dependent - | Defined of global_reference + | Defined of GlobRef.t let obligations_message rem = if rem > 0 then @@ -770,7 +770,7 @@ let update_obls prg obls rem = let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in if List.for_all (fun x -> obligations_solved x) progs then let kn = declare_mutual_definition progs in - Defined (ConstRef kn) + Defined (GlobRef.ConstRef kn) else Dependent) let is_defined obls x = not (Option.is_empty obls.(x).obl_body) @@ -849,12 +849,12 @@ let obligation_terminator name num guard hook auto pf = let obl = obls.(num) in let status = match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () - | (true, _), Vernacexpr.Opaque -> err_not_transp () - | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> + | (_, Evar_kinds.Expand), Opaque -> err_not_transp () + | (true, _), Opaque -> err_not_transp () + | (false, _), Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Transparent -> Evar_kinds.Define false - | (_, status), Vernacexpr.Transparent -> status + | (_, status), Transparent -> status in let obl = { obl with obl_status = false, status } in let ctx = @@ -891,7 +891,7 @@ let obligation_terminator name num guard hook auto pf = let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in - let cst = match gr with ConstRef cst -> cst | _ -> assert false in + let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in let () = match obl.obl_status with (true, Evar_kinds.Expand) diff --git a/vernac/obligations.mli b/vernac/obligations.mli index cc2cacd865..4b6165fb19 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,7 +12,6 @@ open Environ open Constr open Evd open Names -open Globnames (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof @@ -49,7 +48,7 @@ type obligation_info = type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) | Dependent (* Dependent on other definitions *) - | Defined of global_reference (* Defined as id *) + | Defined of GlobRef.t (* Defined as id *) val default_tactic : unit Proofview.tactic ref diff --git a/vernac/record.ml b/vernac/record.ml index 78e68e8a30..bf6affd5f8 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -122,7 +122,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env = EConstr.push_rel_context newps env0 in let poly = match t with - | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in + | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with @@ -168,7 +168,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in - let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in let typ = EConstr.to_constr sigma typ in @@ -316,7 +316,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u let gr = Nametab.locate (Libnames.qualid_of_ident fid) in let kn = destConstRef gr in Declare.definition_message fid; - Universes.register_universe_binders gr ubinders; + UnivNames.register_universe_binders gr ubinders; kn, mkProj (Projection.make kn false,mkRel 1) else let ccl = subst_projection fid subst ti in @@ -352,7 +352,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u applist (mkConstU (kn,u),proj_args) in Declare.definition_message fid; - Universes.register_universe_binders (ConstRef kn) ubinders; + UnivNames.register_universe_binders (ConstRef kn) ubinders; kn, constr_fip with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) @@ -465,9 +465,9 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref [paramimpls]; - Universes.register_universe_binders cref ubinders; + UnivNames.register_universe_binders cref ubinders; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - Universes.register_universe_binders (ConstRef proj_cst) ubinders; + UnivNames.register_universe_binders (ConstRef proj_cst) ubinders; Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = match List.hd coers with | Some b -> Some ((if b then Backward else Forward), List.hd priorities) diff --git a/vernac/record.mli b/vernac/record.mli index 992da2aa58..b2c039f0b5 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -11,7 +11,6 @@ open Names open Vernacexpr open Constrexpr -open Globnames val primitive_flag : bool ref @@ -21,7 +20,7 @@ val declare_projections : ?kind:Decl_kinds.definition_object_kind -> Id.t -> bool list -> - Universes.universe_binders -> + UnivNames.universe_binders -> Impargs.manual_implicits list -> Context.Rel.t -> (Name.t * bool) list * Constant.t option list @@ -30,6 +29,6 @@ val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * - Id.t * constr_expr option -> global_reference + Id.t * constr_expr option -> GlobRef.t -val declare_existing_class : global_reference -> unit +val declare_existing_class : GlobRef.t -> unit diff --git a/vernac/search.ml b/vernac/search.ml index a2a4fb40f0..6d07187fe0 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -22,8 +22,8 @@ open Nametab module NamedDecl = Context.Named.Declaration -type filter_function = global_reference -> env -> constr -> bool -type display_function = global_reference -> env -> constr -> unit +type filter_function = GlobRef.t -> env -> constr -> bool +type display_function = GlobRef.t -> env -> constr -> unit (* This option restricts the output of [SearchPattern ...], [SearchAbout ...], etc. to the names of the symbols matching the @@ -61,7 +61,7 @@ let iter_named_context_name_type f = List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) (* General search over hypothesis of a goal *) -let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = +let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_hyp idh typ = fn (VarRef idh) env typ in let evmap,e = Pfedit.get_goal_context glnum in @@ -69,7 +69,7 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = iter_named_context_name_type iter_hyp pfctxt (* General search over declarations *) -let iter_declarations (fn : global_reference -> env -> constr -> unit) = +let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_obj (sp, kn) lobj = match object_tag lobj with | "VARIABLE" -> @@ -117,8 +117,7 @@ module ConstrPriority = struct (* The priority is memoised here. Because of the very localised use of this module, it is not worth it making a convenient interface. *) - type t = - Globnames.global_reference * Environ.env * Constr.t * priority + type t = GlobRef.t * Environ.env * Constr.t * priority and priority = int module ConstrSet = CSet.Make(Constr) diff --git a/vernac/search.mli b/vernac/search.mli index a1fb7ed3ee..0dc82c1c3f 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -12,7 +12,6 @@ open Names open Constr open Environ open Pattern -open Globnames (** {6 Search facilities. } *) @@ -20,8 +19,8 @@ type glob_search_about_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string -type filter_function = global_reference -> env -> constr -> bool -type display_function = global_reference -> env -> constr -> unit +type filter_function = GlobRef.t -> env -> constr -> bool +type display_function = GlobRef.t -> env -> constr -> unit (** {6 Generic filter functions} *) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 055f6676e8..609dac69aa 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -89,12 +89,14 @@ let set_margin v = Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; Format.pp_set_margin !deep_ft v; + Format.pp_set_margin !err_ft v; (* Heuristic, based on usage: the column on the right of max_indent column is 20% of width, capped to 30 characters *) let m = max (64 * v / 100) (v-30) in Format.pp_set_max_indent Format.str_formatter m; Format.pp_set_max_indent !std_ft m; - Format.pp_set_max_indent !deep_ft m + Format.pp_set_max_indent !deep_ft m; + Format.pp_set_max_indent !err_ft m (** Console display of feedback *) @@ -289,6 +291,14 @@ let init_terminal_output ~color = let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* This is specific to the toplevel *) + +type execution_phase = + | ParsingCommandLine + | Initialization + | LoadingPrelude + | LoadingRcFile + | InteractiveLoop + let pr_loc loc = let fname = loc.Loc.fname in match fname with @@ -301,13 +311,28 @@ let pr_loc loc = int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ str":") -let print_err_exn ?extra any = +let pr_phase ?loc phase = + match phase, loc with + | LoadingRcFile, loc -> + (* For when all errors go through feedback: + str "While loading rcfile:" ++ + Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc *) + Option.map pr_loc loc + | LoadingPrelude, loc -> + Some (str "While loading initial state:" ++ Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc) + | _, Some loc -> Some (pr_loc loc) + | ParsingCommandLine, _ + | Initialization, _ -> None + | InteractiveLoop, _ -> + (* Note: interactive messages such as "foo is defined" are not located *) + None + +let print_err_exn phase any = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in - let msg_loc = Option.cata pr_loc (mt ()) loc in - let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in + let pre_hdr = pr_phase ?loc phase in let msg = CErrors.iprint (e, info) ++ fnl () in - std_logger ~pre_hdr Feedback.Error msg + std_logger ?pre_hdr Feedback.Error msg let with_output_to_file fname func input = let channel = open_out (String.concat "." [fname; "out"]) in diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 579b456a28..73dcb0064b 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -53,8 +53,17 @@ val init_terminal_output : color:bool -> unit (** Error printing *) (* To be deprecated when we can fully move to feedback-based error printing. *) + +type execution_phase = + | ParsingCommandLine + | Initialization + | LoadingPrelude + | LoadingRcFile + | InteractiveLoop + val pr_loc : Loc.t -> Pp.t -val print_err_exn : ?extra:Pp.t -> exn -> unit +val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option +val print_err_exn : execution_phase -> exn -> unit (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a9d1631bae..e1ce4e194c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -518,7 +518,7 @@ let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) let status = Pfedit.by (Tactics.exact_proof c) in - save_proof (Vernacexpr.(Proved(Opaque,None))); + save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = @@ -672,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Enforce mty_ast) [] + id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); @@ -855,7 +855,7 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint inst false "inst"; + Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; let program_mode = Flags.is_program_mode () in ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) @@ -909,7 +909,7 @@ let vernac_set_used_variables e = if List.is_empty to_clear then (p, ()) else let tac = Tactics.clear to_clear in - fst (Pfedit.solve SelectAll None tac p), () + fst (Pfedit.solve Goal_select.SelectAll None tac p), () end (*****************************) @@ -1268,7 +1268,7 @@ let vernac_reserve bl = let vernac_generalizable ~atts = let local = make_non_locality atts.locality in - Implicit_quantifiers.declare_generalizable local + Implicit_quantifiers.declare_generalizable ~local let _ = declare_bool_option @@ -1465,22 +1465,22 @@ let _ = optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } - + let _ = declare_bool_option { optdepr = false; optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; - optread = Flags.get_dump_bytecode; - optwrite = Flags.set_dump_bytecode } + optread = (fun () -> !Cbytegen.dump_bytecode); + optwrite = (:=) Cbytegen.dump_bytecode } let _ = declare_bool_option { optdepr = false; optname = "dumping VM lambda code after compilation"; optkey = ["Dump";"Lambda"]; - optread = Flags.get_dump_lambda; - optwrite = Flags.set_dump_lambda } + optread = (fun () -> !Clambda.dump_lambda); + optwrite = (:=) Clambda.dump_lambda } let _ = declare_bool_option @@ -1611,7 +1611,7 @@ let get_current_context_of_args = function let query_command_selector ?loc = function | None -> None - | Some (SelectNth n) -> Some n + | Some (Goal_select.SelectNth n) -> Some n | _ -> user_err ?loc ~hdr:"query_command_selector" (str "Query commands only support the single numbered goal selector.") @@ -1619,17 +1619,16 @@ let vernac_check_may_eval ~atts redexp glopt rc = let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in - let c = EConstr.Unsafe.to_constr c in let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; - let sigma',nf = Evarutil.nf_evars_and_universes sigma' in + let sigma' = Evd.minimize_universes sigma' in let uctx = Evd.universe_context_set sigma' in let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in - let c = nf c in let j = - if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) + if Evarutil.has_undefined_evars sigma' c then + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) else + let c = EConstr.to_constr sigma' c in (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in @@ -1742,7 +1741,7 @@ let vernac_print ~atts env sigma = else str"There may remain asynchronous universe constraints" in begin match dst with - | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining + | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining | Some s -> dump_universes_gen univ s end | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) @@ -1912,7 +1911,7 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p | _ -> user_err ~hdr:"bracket_selector" (str "Brackets only support the single numbered goal selector.")) @@ -2244,7 +2243,7 @@ let with_fail st b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info + if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end |