From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- toplevel/assumptions.ml | 4 ++-- toplevel/assumptions.mli | 2 +- toplevel/auto_ind_decl.ml | 2 +- toplevel/auto_ind_decl.mli | 2 +- toplevel/cerrors.ml | 2 +- toplevel/cerrors.mli | 2 +- toplevel/class.ml | 2 +- toplevel/class.mli | 2 +- toplevel/classes.ml | 4 ++-- toplevel/classes.mli | 2 +- toplevel/command.ml | 13 ++++++++----- toplevel/command.mli | 2 +- toplevel/coqinit.ml | 2 +- toplevel/coqinit.mli | 2 +- toplevel/coqloop.ml | 2 +- toplevel/coqloop.mli | 2 +- toplevel/coqtop.ml | 11 ++++++++--- toplevel/coqtop.mli | 2 +- toplevel/discharge.ml | 2 +- toplevel/discharge.mli | 2 +- toplevel/g_obligations.ml4 | 2 +- toplevel/himsg.ml | 9 ++++++++- toplevel/himsg.mli | 2 +- toplevel/ind_tables.ml | 2 +- toplevel/ind_tables.mli | 2 +- toplevel/indschemes.ml | 23 ++++++++++++++++------- toplevel/indschemes.mli | 2 +- toplevel/locality.ml | 2 +- toplevel/locality.mli | 2 +- toplevel/metasyntax.ml | 2 +- toplevel/metasyntax.mli | 2 +- toplevel/mltop.ml | 2 +- toplevel/mltop.mli | 2 +- toplevel/obligations.ml | 43 +++++++++++++++++++++++++++---------------- toplevel/obligations.mli | 6 +++--- toplevel/record.ml | 2 +- toplevel/record.mli | 2 +- toplevel/search.ml | 2 +- toplevel/search.mli | 2 +- toplevel/usage.ml | 5 ++++- toplevel/usage.mli | 2 +- toplevel/vernac.ml | 8 +++++++- toplevel/vernac.mli | 6 +++++- toplevel/vernacentries.ml | 21 ++++++++++----------- toplevel/vernacentries.mli | 2 +- toplevel/vernacinterp.ml | 2 +- toplevel/vernacinterp.mli | 2 +- 47 files changed, 135 insertions(+), 88 deletions(-) (limited to 'toplevel') diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index a6bd968e..2a3e6536 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (* non dependent match on an inductive with no constructors *) begin match Constr.(kind oty, kind c) with - | Lambda(Anonymous,_,oty), Const (kn, _) + | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> let body () = Global.body_of_constant_body (lookup_constant kn) in diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli index 9c9f81bd..666218fe 100644 --- a/toplevel/assumptions.mli +++ b/toplevel/assumptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; Typeclasses.declare_instance pri (not global) (ConstRef cst) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 2b7e9e4f..24c51b31 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Lemmas.call_hook (fun exn -> exn) hook l r) in ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in @@ -1010,7 +1011,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in - let hook l gr = + let hook l gr _ = let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let pl, univs = Evd.universe_context !evdref in @@ -1026,7 +1027,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook l gr = + let hook l gr _ = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in hook, recname, typ @@ -1127,7 +1128,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -1163,7 +1165,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in diff --git a/toplevel/command.mli b/toplevel/command.mli index 8e2d9c6f..b97cb487 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* add_require "Coq.Compat.Coq84" + | _ -> () + let compile_list = ref ([] : (bool * string) list) let glob_opt = ref false @@ -475,7 +480,7 @@ let parse_args arglist = |"-async-proofs-private-flags" -> Flags.async_proofs_private_flags := Some (next ()); |"-worker-id" -> set_worker_id opt (next ()) - |"-compat" -> Flags.compat_version := get_compat_version (next ()) + |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v |"-compile" -> add_compile false (next ()) |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true @@ -541,6 +546,7 @@ let parse_args arglist = |"-v"|"--version" -> Usage.version (exitcode ()) |"-verbose-compat-notations" -> verb_compat_ntn := true |"-where" -> print_where := true + |"-xml" -> Flags.xml_export := true (* Deprecated options *) |"-byte" -> warning "option -byte deprecated, call with .byte suffix" @@ -556,7 +562,6 @@ let parse_args arglist = |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"." |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ()) |"-quality" -> warning "Obsolete option \"-quality\"." - |"-xml" -> warning "Obsolete option \"-xml\"." (* Unknown option *) | s -> extras := s :: !extras diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 67044745..c9d1ba45 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* explain_signature_mismatch l spec err | LabelAlreadyDeclared l -> explain_label_already_declared l @@ -940,6 +946,7 @@ let explain_module_error = function | IncorrectWithConstraint l -> explain_incorrect_label_constraint l | GenerativeModuleExpected l -> explain_generative_module_expected l | LabelMissing (l,s) -> explain_label_missing l s + | IncludeRestrictedFunctor mp -> explain_include_restricted_functor mp (* Module internalization errors *) diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 3d5442bb..3ef98380 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* f) lnamedepindsort and env0 = Global.env() in - let sigma, lrecspec = + let sigma, lrecspec, _ = List.fold_right - (fun (_,dep,ind,sort) (evd, l) -> - let evd, indu = Evd.fresh_inductive_instance env0 evd ind in - (evd, (indu,dep,interp_elimination_sort sort) :: l)) - lnamedepindsort (Evd.from_env env0,[]) + (fun (_,dep,ind,sort) (evd, l, inst) -> + let evd, indu, inst = + match inst with + | None -> + let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in + let ctxs = Univ.ContextSet.of_context ctx in + let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in + let u = Univ.UContext.instance ctx in + evd, (ind,u), Some u + | Some ui -> evd, (ind, ui), inst + in + (evd, (indu,dep,interp_elimination_sort sort) :: l, inst)) + lnamedepindsort (Evd.from_env env0,[],None) in let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index 98746107..e5d79fd5 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr; - prg_hook : unit Lemmas.declaration_hook; + prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook; prg_opaque : bool; + prg_sign: named_context_val; } type program_info = program_info_aux Ephemeron.key @@ -517,7 +518,7 @@ let declare_definition prg = progmap_remove prg; !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r)) + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) open Pp @@ -582,6 +583,7 @@ let declare_mutual_definition l = in (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in + let fix_exn = Stm.get_fix_exn () in let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) @@ -589,8 +591,8 @@ let declare_mutual_definition l = Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in let kn = match gr with ConstRef kn -> kn | _ -> assert false in - Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr; - List.iter progmap_remove l; kn + Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; + List.iter progmap_remove l; kn let shrink_body c = let ctx, b = decompose_lam c in @@ -642,7 +644,7 @@ let declare_obligation prg obl body ty uctx = else Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) } -let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook = +let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls impls kind reduce hook = let obls', b = match b with | None -> @@ -666,8 +668,8 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; - prg_hook = hook; - prg_opaque = opaque; } + prg_hook = hook; prg_opaque = opaque; + prg_sign = sign } let map_cardinal m = let i = ref 0 in @@ -822,7 +824,9 @@ let obligation_hook prg obl num auto ctx' _ gr = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - Evd.evar_universe_context (Evd.from_env (Global.env ())) + let evd = Evd.from_env (Global.env ()) in + let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in + Evd.evar_universe_context ctx' else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -853,9 +857,10 @@ let rec solve_obligation prg num tac = let obl = subst_deps_obl obls obl in let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in let _ = Pfedit.by (snd (get_default_tactic ())) in @@ -889,17 +894,21 @@ and solve_obligation_by_tac prg obls i tac = | Some t -> t | None -> snd (get_default_tactic ()) in + let evd = Evd.from_ctx !prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 !prg.prg_kind) !prg.prg_ctx + (pi2 !prg.prg_kind) (Evd.evar_universe_context evd) in let uctx = Evd.evar_context_universe_context ctx in let () = prg := {!prg with prg_ctx = ctx} in let def, obl' = declare_obligation !prg obl t ty uctx in obls.(i) <- obl'; if def && not (pi2 !prg.prg_kind) then ( - (* Declare the term constraints with the first obligation only *) - let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + (* Declare the term constraints with the first obligation only *) + let evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in prg := {!prg with prg_ctx = ctx'}); true else false @@ -987,9 +996,10 @@ let show_term n = ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic - ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls = + ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = + let sign = Decls.initialize_named_context_for_proof () in let info = str (Id.to_string n) ++ str " has type-checked" in - let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in + let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose msg_info (info ++ str "."); @@ -1005,11 +1015,12 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) | _ -> res) let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) - ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind = + ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = + let sign = Decls.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> - let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind) + let prg = init_prog_info sign ~opaque n (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook in progmap_add n (Ephemeron.create prg)) l; let _defined = diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 61a8ee52..b2320a57 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ?term:Term.constr -> Term.types -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(Term.constr -> Term.constr) -> - ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress + ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -84,7 +84,7 @@ val add_mutual_definitions : ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> - ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> + ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index dc2c9264..04da628c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let long_f_dot_v = ensure_v f in diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index affc2171..008d7a31 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit +(** Set XML hooks *) +val xml_start_library : (unit -> unit) Hook.t +val xml_end_library : (unit -> unit) Hook.t + (** Load a vernac file, verbosely or not. Errors are annotated with file and location *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b6a1a53f..72dd967b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) - | PrintUniverses (b, None) -> + | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then Univ.sort_universes univ else univ in let pr_remaining = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in - msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) - | PrintUniverses (b, Some s) -> dump_universes b s + begin match dst with + | None -> msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + | Some s -> dump_universes_gen univ s + end | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) @@ -2051,7 +2048,7 @@ let check_vernac_supports_polymorphism c p = let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () - | Some b -> b + | Some b -> Flags.make_polymorphic_flag b; b (** A global default timeout, controled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2152,7 +2149,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = 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 + Flags.program_mode := orig_program_mode; + ignore (Flags.use_polymorphic_flag ()) end with | reraise when @@ -2164,6 +2162,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = let e = locate_if_not_already loc e in let () = restore_timeout () in Flags.program_mode := orig_program_mode; + ignore (Flags.use_polymorphic_flag ()); iraise e and aux_list ?locality ?polymorphism isprogcmd l = List.iter (aux false) (List.map snd l) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index c6d87596..451ccdb4 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*