diff options
| author | Maxime Dénès | 2019-03-28 13:36:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-28 13:36:52 +0100 |
| commit | 688e20c432d2639050a62703e1c566ddfbe42b2a (patch) | |
| tree | 3b34d3bd3b73a42a8eb730a3bb6c0e6a5cb00a5f /plugins | |
| parent | 6d0ffe795f6f29730d59c379285201fd46023935 (diff) | |
| parent | 91dfe5163fd4405977ad8fc8fe178ba5bcd73c88 (diff) | |
Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
Diffstat (limited to 'plugins')
40 files changed, 601 insertions, 597 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 978969bf59..5066c3931d 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -255,5 +255,3 @@ val find_contradiction : UF.t -> (Names.Id.t * (int * int)) list -> (Names.Id.t * (int * int)) *) - - diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index afdbfa1999..4425e41652 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -101,8 +101,7 @@ let start_deriving f suchthat lemma = in let terminator = Proof_global.make_terminator terminator in - let () = Proof_global.start_dependent_proof lemma kind goals terminator in - let _ = Proof_global.with_current_proof begin fun _ p -> + let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in + fst @@ Proof_global.with_current_proof begin fun _ p -> Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p - end in - () + end pstate diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 06ff9c48cf..6bb923118e 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,4 @@ (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> unit +val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 0cdf8fb5d8..214a9d8bb5 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -23,6 +23,6 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { Derive.start_deriving f suchthat lemma } +| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> + { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) } END diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 0fa9be21c9..8f17f7b2dd 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -750,16 +750,19 @@ let extract_and_compile l = Feedback.msg_notice (str "Extracted code successfully compiled") (* Show the extraction of the current ongoing proof *) - -let show_extraction () = +let show_extraction ~pstate = + let pstate = match pstate with + | None -> CErrors.user_err Pp.(str "No ongoing proof") + | Some pstate -> pstate + in init ~inner:true false false; - let prf = Proof_global.give_me_the_proof () in - let sigma, env = Pfedit.get_current_context () in + let prf = Proof_global.give_me_the_proof pstate in + let sigma, env = Pfedit.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in - let l = Label.of_id (Proof_global.get_current_proof_name ()) in + let l = Label.of_id (Proof_global.get_current_proof_name pstate) in let fake_ref = ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 54fde2ca46..7ba7e05019 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : unit -> unit +val show_extraction : pstate:Proof_global.t option -> unit diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index 1445dffefa..d7bb27f121 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -178,6 +178,6 @@ END (* Show the extraction of the current proof *) VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| [ "Show" "Extraction" ] - -> { show_extraction () } +| ![ proof ] [ "Show" "Extraction" ] + -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } END diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 16f376931e..287a374ab1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -722,7 +722,7 @@ let build_proof (treat_new_case ptes_infos nb_instantiate_partial - (build_proof env sigma do_finalize) + (build_proof do_finalize) t dyn_infos) g' @@ -733,7 +733,7 @@ let build_proof ] g in - build_proof env sigma do_finalize_t {dyn_infos with info = t} g + build_proof do_finalize_t {dyn_infos with info = t} g | Lambda(n,t,b) -> begin match EConstr.kind sigma (pf_concl g) with @@ -749,7 +749,7 @@ let build_proof in let new_infos = {dyn_infos with info = new_term} in let do_prove new_hyps = - build_proof env sigma do_finalize + build_proof do_finalize {new_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps @@ -762,7 +762,7 @@ let build_proof do_finalize dyn_infos g end | Cast(t,_,_) -> - build_proof env sigma do_finalize {dyn_infos with info = t} g + build_proof do_finalize {dyn_infos with info = t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> do_finalize dyn_infos g | App(_,_) -> @@ -792,7 +792,7 @@ let build_proof | Lambda _ -> let new_term = Reductionops.nf_beta env sigma dyn_infos.info in - build_proof env sigma do_finalize {dyn_infos with info = new_term} + build_proof do_finalize {dyn_infos with info = new_term} g | LetIn _ -> let new_infos = @@ -805,11 +805,11 @@ let build_proof h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; h_reduce_with_zeta Locusops.onConcl; - build_proof env sigma do_finalize new_infos + build_proof do_finalize new_infos ] g | Cast(b,_,_) -> - build_proof env sigma do_finalize {dyn_infos with info = b } g + build_proof do_finalize {dyn_infos with info = b } g | Case _ | Fix _ | CoFix _ -> let new_finalize dyn_infos = let new_infos = @@ -819,7 +819,7 @@ let build_proof in build_proof_args env sigma do_finalize new_infos in - build_proof env sigma new_finalize {dyn_infos with info = f } g + build_proof new_finalize {dyn_infos with info = f } g end | Fix _ | CoFix _ -> user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) @@ -839,12 +839,12 @@ let build_proof (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; h_reduce_with_zeta Locusops.onConcl; - build_proof env sigma do_finalize new_infos + build_proof do_finalize new_infos ] g | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") - and build_proof env sigma do_finalize dyn_infos g = + and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + observe_tac_stream (str "build_proof with " ++ pr_leconstr_env (pf_env g) (project g) dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g and build_proof_args env sigma do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -866,7 +866,7 @@ let build_proof {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} ) in - build_proof env sigma do_finalize + build_proof do_finalize {dyn_infos with info = arg } g in @@ -879,19 +879,7 @@ let build_proof in (* observe_tac "build_proof" *) fun g -> - let env = pf_env g in - let sigma = project g in - build_proof env sigma (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g - - - - - - - - - - + build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g (* Proof of principles from structural functions *) @@ -1002,19 +990,18 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) - Lemmas.start_proof + let pstate = Lemmas.start_proof ~ontop:None (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) (mk_equation_id f_id) (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) evd - lemma_type; - ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); - evd - - + lemma_type + in + let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in + let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + pstate, evd let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = @@ -1028,7 +1015,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a Ensures by: obvious i*) let equation_lemma_id = (mk_equation_id f_id) in - evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; + evd := snd @@ generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with | Option.IsNone -> diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1217ba0eba..e9a2c285d0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -308,31 +308,30 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in - begin - Lemmas.start_proof + let pstate = + Lemmas.start_proof ~ontop:None new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (EConstr.of_constr new_principle_type) - ; - (* let _tim1 = System.get_time () in *) - let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in - ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams))); - (* let _tim2 = System.get_time () in *) - (* begin *) - (* let dur1 = System.time_difference tim1 tim2 in *) - (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) - (* end; *) + in + (* let _tim1 = System.get_time () in *) + let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in + let pstate,_ = Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) pstate in + (* let _tim2 = System.get_time () in *) + (* begin *) + (* let dur1 = System.time_difference tim1 tim2 in *) + (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) + (* end; *) - let open Proof_global in - let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in - match entries with - | [entry] -> - discard_current (); - (id,(entry,persistence)), hook - | _ -> - CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") - end + let open Proof_global in + let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in + match entries with + | [entry] -> + let pstate = discard_current pstate in + (id,(entry,persistence)), hook, pstate + | _ -> + CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof @@ -382,7 +381,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort InProp; register_with_sort InSet in - let ((id,(entry,g_kind)),hook) = + let ((id,(entry,g_kind)),hook,pstate) = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -390,25 +389,9 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - save false new_princ_name entry ~hook uctx g_kind + save new_princ_name entry ~hook uctx g_kind with e when CErrors.noncritical e -> - begin - begin - try - let id = Proof_global.get_current_proof_name () in - let s = Id.to_string id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.equal (String.sub s 0 n) "___________princ_________" - then Proof_global.discard_current () - else () - else () - with e when CErrors.noncritical e -> () - end; - raise (Defining_principle e) - end -(* defined () *) - + raise (Defining_principle e) exception Not_Rec @@ -537,7 +520,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in - let ((_,(const,_)),_) = + let ((_,(const,_)),_,pstate) = try build_functional_principle evd false first_type @@ -547,21 +530,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) (fun _ _ _ _ _ -> ()) with e when CErrors.noncritical e -> - begin - begin - try - let id = Proof_global.get_current_proof_name () in - let s = Id.to_string id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.equal (String.sub s 0 n) "___________princ_________" - then Proof_global.discard_current () - else () - else () - with e when CErrors.noncritical e -> () - end; - raise (Defining_principle e) - end + raise (Defining_principle e) in incr i; @@ -611,7 +580,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let ((_,(const,_)),_) = + let ((_,(const,_)),_,pstate) = build_functional_principle evd false diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 6f67ab4d8b..4e8cf80ed2 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -177,7 +177,7 @@ let () = (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function -| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] +| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] => { let hard = List.exists (function | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in @@ -223,37 +223,34 @@ let warning_error names e = } VERNAC COMMAND EXTEND NewFunctionalScheme -| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] +| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - { + { fun ~pstate -> begin - try - Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - begin - match fas with - | (_,fun_name,_)::_ -> - begin - begin - make_graph (Smartlocate.global_with_alias fun_name) - end - ; - try Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - CErrors.user_err Pp.(str "Cannot generate induction principle(s)") - | e when CErrors.noncritical e -> - let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e - - end + try + Functional_principles_types.build_scheme fas; pstate + with + | Functional_principles_types.No_graph_found -> + begin + match fas with + | (_,fun_name,_)::_ -> + begin + let pstate = make_graph ~pstate (Smartlocate.global_with_alias fun_name) in + try Functional_principles_types.build_scheme fas; pstate + with + | Functional_principles_types.No_graph_found -> + CErrors.user_err Pp.(str "Cannot generate induction principle(s)") + | e when CErrors.noncritical e -> + let names = List.map (fun (_,na,_) -> na) fas in + warning_error names e; pstate + end | _ -> assert false (* we can only have non empty list *) - end - | e when CErrors.noncritical e -> - let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e + end + | e when CErrors.noncritical e -> + let names = List.map (fun (_,na,_) -> na) fas in + warning_error names e; pstate end - } END (***** debug only ***) @@ -266,5 +263,6 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) } +| ![ proof ] ["Generate" "graph" "for" reference(c)] -> + { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f4807954a7..275b58f0aa 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -369,7 +369,7 @@ let add_pat_variables sigma pat typ env : Environ.env = let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in - let new_env = add_pat_variables env pat typ in + let new_env = add_pat_variables env pat typ in let res = fst ( Context.Rel.fold_outside diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index b69ca7080c..a5c19f3217 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -410,11 +410,11 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - ComDefinition.do_definition + ComDefinition.do_definition ~ontop:pstate ~program_mode:false fname (Decl_kinds.Global,false,Decl_kinds.Definition) pl @@ -432,9 +432,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - evd,List.rev rev_pconstants + pstate, evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint Global false fixpoint_exprl; + let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -448,8 +448,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - evd,List.rev rev_pconstants - + pstate,evd,List.rev rev_pconstants + let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -638,10 +638,10 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex fixpoint_exprl_with_new_bl -let do_generate_principle pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit = +let do_generate_principle ~pstate pconstants on_error register_built interactive_proof + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; - let _is_struct = + let pstate, _is_struct = match fixpoint_exprl with | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = @@ -665,8 +665,8 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; - false + then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, false + else pstate, false |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with @@ -689,8 +689,8 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; - true + then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true + else pstate, true | _ -> List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> match ord with @@ -707,10 +707,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in - let evd,pconstants = + let pstate,evd,pconstants = if register_built - then register_struct is_rec fixpoint_exprl - else (Evd.from_env (Global.env ()),pconstants) + then register_struct ~pstate is_rec fixpoint_exprl + else pstate, Evd.from_env (Global.env ()), pconstants in let evd = ref evd in generate_principle @@ -723,10 +723,11 @@ let do_generate_principle pconstants on_error register_built interactive_proof recdefs interactive_proof (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); - if register_built then begin derive_inversion fix_names; end; - true; + if register_built then + begin derive_inversion fix_names; end; + pstate, true in - () + pstate let rec add_args id new_args = CAst.map (function | CRef (qid,_) as b -> @@ -843,13 +844,14 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph (f_ref : GlobRef.t) = +let make_graph ~pstate (f_ref : GlobRef.t) = + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in let c,c_body = match f_ref with | ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> - let sigma, env = Pfedit.get_current_context () in raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) end | _ -> raise (UserError (None, str "Not a function reference") ) @@ -857,8 +859,7 @@ let make_graph (f_ref : GlobRef.t) = (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" | Some (body, _) -> - let env = Global.env () in - let sigma = Evd.from_env env in + let env = Global.env () in let extern_body,extern_type = with_full_print (fun () -> (Constrextern.extern_constr false env sigma (EConstr.of_constr body), @@ -902,12 +903,11 @@ let make_graph (f_ref : GlobRef.t) = [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp = Constant.modpath c in - do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; + let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in (* We register the infos *) List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list) + expr_list; + pstate) let do_generate_principle = do_generate_principle [] warning_error true - - diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index f209fb19fd..acf85f539e 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,18 +5,16 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : - bool -> - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - unit - +val do_generate_principle : pstate:Proof_global.t option -> + bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> + Proof_global.t option -val functional_induction : +val functional_induction : bool -> EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - -val make_graph : GlobRef.t -> unit +val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e34323abf4..40f66ce5eb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const ?hook uctx (locality,_,kind) = +let save id const ?hook uctx (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -143,7 +143,6 @@ let save with_clean id const ?hook uctx (locality,_,kind) = let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in - if with_clean then Proof_global.discard_current (); Lemmas.call_hook ?hook ~fix_exn uctx [] l r; definition_message id diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 12facc5744..9670cf1fa7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -43,8 +43,7 @@ val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr val save - : bool - -> Id.t + : Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> UState.t @@ -78,15 +77,12 @@ val find_Function_infos : Constant.t -> function_info val find_Function_of_graph : inductive -> function_info (* WARNING: To be used just after the graph definition !!! *) val add_Function : bool -> Constant.t -> unit - val update_Function : function_info -> unit - (** debugging *) val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t val pr_table : Environ.env -> Evd.evar_map -> Pp.t - (* val function_debug : bool ref *) val do_observe : unit -> bool val do_rewrite_dependent : unit -> bool diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 37dbfec4c9..edb698280f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -802,16 +802,16 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_correct_id f_id in - let (typ,_) = lemmas_types_infos.(i) in - Lemmas.start_proof + let (typ,_) = lemmas_types_infos.(i) in + let pstate = Lemmas.start_proof ~ontop:None lem_id (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd - typ; - ignore (Pfedit.by + typ in + let pstate = fst @@ Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") - (proving_tac i)))); - (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); + (proving_tac i))) pstate in + let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -865,13 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - Lemmas.start_proof lem_id + let pstate = Lemmas.start_proof ~ontop:None lem_id (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma - (fst lemmas_types_infos.(i)); - ignore (Pfedit.by + (fst lemmas_types_infos.(i)) in + let pstate = fst (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i)))) ; - (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); + (proving_tac i))) pstate) in + let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e19741a4e9..3c2b03dfe0 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None))) +let defined pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -228,6 +228,7 @@ let observe strm = let do_observe_tac s tac g = let goal = Printer.pr_goal g in + let s = s (pf_env g) (project g) in let lmsg = (str "recdef : ") ++ s in observe (s++fnl()); Stack.push (lmsg,goal) debug_queue; @@ -252,8 +253,8 @@ let observe_tclTHENLIST s tacl = then let rec aux n = function | [] -> tclIDTAC - | [tac] -> observe_tac (s ++ spc () ++ int n) tac - | tac::tacl -> observe_tac (s ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl)) + | [tac] -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) tac + | tac::tacl -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl)) in aux 0 tacl else tclTHENLIST tacl @@ -268,11 +269,11 @@ let tclUSER tac is_mes l g = | None -> tclIDTAC | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l) in - observe_tclTHENLIST (str "tclUSER1") + observe_tclTHENLIST (fun _ _ -> str "tclUSER1") [ clear_tac; if is_mes - then observe_tclTHENLIST (str "tclUSER2") + then observe_tclTHENLIST (fun _ _ -> str "tclUSER2") [ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force Indfun_common.ltof_ref))]); @@ -394,12 +395,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = ) [] rev_context in let rev_ids = pf_get_new_ids (List.rev ids) g in let new_b = substl (List.map mkVar rev_ids) b in - observe_tclTHENLIST (str "treat_case1") + observe_tclTHENLIST (fun _ _ -> str "treat_case1") [ h_intros (List.rev rev_ids); Proofview.V82.of_tactic (intro_using teq_id); onLastHypId (fun heq -> - observe_tclTHENLIST (str "treat_case2")[ + observe_tclTHENLIST (fun _ _ -> str "treat_case2")[ Proofview.V82.of_tactic (clear to_intros); h_intros to_intros; (fun g' -> @@ -426,6 +427,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = let sigma = project g in + let env = pf_env g in match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") | Proj _ -> user_err Pp.(str "Function cannot treat projections") @@ -441,18 +443,18 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = | Prod _ -> begin try - check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Lambda(n,t,b) -> begin try - check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -480,8 +482,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g - | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> @@ -503,10 +505,9 @@ and travel_args jinfo is_final continuation_tac infos = travel jinfo new_continuation_tac {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = - fun g -> observe_tac - (str jinfo.message ++ Printer.pr_leconstr_env (pf_env g) (project g) expr_info.info) - (travel_aux jinfo continuation_tac expr_info) g + (fun env sigma -> str jinfo.message ++ Printer.pr_leconstr_env env sigma expr_info.info) + (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) @@ -527,16 +528,16 @@ let rec prove_lt hyple g = in let y = List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in - observe_tclTHENLIST (str "prove_lt1")[ + observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); - observe_tac (str "prove_lt") (prove_lt hyple) + observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ] with Not_found -> ( ( - observe_tclTHENLIST (str "prove_lt2")[ + observe_tclTHENLIST (fun _ _ -> str "prove_lt2")[ Proofview.V82.of_tactic (apply (delayed_force lt_S_n)); - (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption)) + (observe_tac (fun _ _ -> str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption)) ]) ) end @@ -552,26 +553,26 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = let h' = next_ident_away_in_goal (h'_id) ids in let ids = h'::ids in let def = next_ident_away_in_goal def_id ids in - observe_tclTHENLIST (str "destruct_bounds_aux1")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux1")[ Proofview.V82.of_tactic (split (ImplicitBindings [s_max])); Proofview.V82.of_tactic (intro_then (fun id -> Proofview.V82.tactic begin - observe_tac (str "destruct_bounds_aux") + observe_tac (fun _ _ -> str "destruct_bounds_aux") (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id))) [ - observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id); + observe_tclTHENLIST (fun _ _ -> str "")[Proofview.V82.of_tactic (intro_using h_id); Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]))); Proofview.V82.of_tactic default_full_auto]; - observe_tclTHENLIST (str "destruct_bounds_aux2")[ - observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id])); + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux2")[ + observe_tac (fun _ _ -> str "clearing k ") (Proofview.V82.of_tactic (clear [id])); h_intros [k;h';def]; - observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); - observe_tac (str "unfold functional") + observe_tac (fun _ _ -> str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); + observe_tac (fun _ _ -> str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference infos.func)])); ( - observe_tclTHENLIST (str "test")[ + observe_tclTHENLIST (fun _ _ -> str "test")[ list_rewrite true (List.fold_right (fun e acc -> (mkVar e,true)::acc) @@ -582,16 +583,16 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *) (* ; *) - (observe_tac (str "finishing") + (observe_tac (fun _ _ -> str "finishing") (tclORELSE (Proofview.V82.of_tactic intros_reflexivity) - (observe_tac (str "calling prove_lt") (prove_lt hyple))))]) + (observe_tac (fun _ _ -> str "calling prove_lt") (prove_lt hyple))))]) ] ] )end)) ] g | (_,v_bound)::l -> - observe_tclTHENLIST (str "destruct_bounds_aux3")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux3")[ Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)); Proofview.V82.of_tactic (clear [v_bound]); tclDO 2 (Proofview.V82.of_tactic intro); @@ -599,7 +600,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = (fun p_hyp -> (onNthHypId 2 (fun p -> - observe_tclTHENLIST (str "destruct_bounds_aux4")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux4")[ Proofview.V82.of_tactic (simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|]))); tclDO 3 (Proofview.V82.of_tactic intro); @@ -623,32 +624,33 @@ let destruct_bounds infos = let terminate_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_app1")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app1")[ continuation_tac infos; - observe_tac (str "first split") + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); - observe_tac (str "destruct_bounds (1)") (destruct_bounds infos) + observe_tac (fun _ _ -> str "destruct_bounds (1)") (destruct_bounds infos) ] else continuation_tac infos let terminate_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_others")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_others")[ continuation_tac infos; - observe_tac (str "first split") + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); - observe_tac (str "destruct_bounds") (destruct_bounds infos) + observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos) ] else continuation_tac infos let terminate_letin (na,b,t,e) expr_info continuation_tac info g = let sigma = project g in + let env = pf_env g in let new_e = subst1 info.info e in let new_forbidden = let forbid = try - check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) b; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) b; true with e when CErrors.noncritical e -> false in @@ -693,7 +695,7 @@ let mkDestructEq : let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> - observe_tclTHENLIST (str "mkDestructEq") + observe_tclTHENLIST (fun _ _ -> str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); (fun g2 -> let changefun patvars env sigma = @@ -705,9 +707,10 @@ let mkDestructEq : let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let sigma = project g in + let env = pf_env g in let f_is_present = try - check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) a; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) a; false with e when CErrors.noncritical e -> true @@ -721,45 +724,46 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') + observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS destruct_tac - (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) + (List.map_i (fun i e -> observe_tac (fun _ _ -> str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) )) with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} ) + (observe_tac (fun _ _ -> str "is computable " ++ Printer.pr_leconstr_env env sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} ) )) g let terminate_app_rec (f,args) expr_info continuation_tac _ g = let sigma = project g in - List.iter (check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids)) + let env = pf_env g in + List.iter (check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids)) args; begin try let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in - observe_tclTHENLIST (str "terminate_app_rec")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec")[ continuation_tac new_infos; if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_app_rec1")[ - observe_tac (str "first split") + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec1")[ + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); - observe_tac (str "destruct_bounds (3)") + observe_tac (fun _ _ -> str "destruct_bounds (3)") (destruct_bounds new_infos) ] else tclIDTAC ] g with Not_found -> - observe_tac (str "terminate_app_rec not found") (tclTHENS + observe_tac (fun _ _ -> str "terminate_app_rec not found") (tclTHENS (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))) [ - observe_tclTHENLIST (str "terminate_app_rec2")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2")[ Proofview.V82.of_tactic (intro_using rec_res_id); Proofview.V82.of_tactic intro; onNthHypId 1 @@ -772,14 +776,14 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ g = (v,v_bound)::expr_info.values_and_bounds; args_assoc=(args,mkVar v)::expr_info.args_assoc } in - observe_tclTHENLIST (str "terminate_app_rec3")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec3")[ continuation_tac new_infos; if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_app_rec4")[ - observe_tac (str "first split") + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec4")[ + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); - observe_tac (str "destruct_bounds (2)") + observe_tac (fun _ _ -> str "destruct_bounds (2)") (destruct_bounds new_infos) ] else @@ -789,12 +793,12 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ g = ) ) ]; - observe_tac (str "proving decreasing") ( + observe_tac (fun _ _ -> str "proving decreasing") ( tclTHENS (* proof of args < formal args *) (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv))) [ - observe_tac (str "assumption") (Proofview.V82.of_tactic assumption); - observe_tclTHENLIST (str "terminate_app_rec5") + observe_tac (fun _ _ -> str "assumption") (Proofview.V82.of_tactic assumption); + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec5") [ tclTRY(list_rewrite true (List.map @@ -830,7 +834,7 @@ let prove_terminate = travel terminate_info (* Equation proof *) let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = - observe_tac (str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos) + observe_tac (fun _ _ -> str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos) let rec prove_le g = let sigma = project g in @@ -856,9 +860,9 @@ let rec prove_le g = let _,args = decompose_app sigma t in List.hd (List.tl args) in - observe_tclTHENLIST (str "prove_le")[ + observe_tclTHENLIST (fun _ _ -> str "prove_le")[ Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|]))); - observe_tac (str "prove_le (rec)") (prove_le) + observe_tac (fun _ _ -> str "prove_le (rec)") (prove_le) ] with Not_found -> tclFAIL 0 (mt()) end; @@ -868,8 +872,8 @@ let rec prove_le g = let rec make_rewrite_list expr_info max = function | [] -> tclIDTAC | (_,p,hp)::l -> - observe_tac (str "make_rewrite_list") (tclTHENS - (observe_tac (str "rewrite heq on " ++ Id.print p ) ( + observe_tac (fun _ _ -> str "make_rewrite_list") (tclTHENS + (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) ( (fun g -> let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in @@ -886,16 +890,16 @@ let rec make_rewrite_list expr_info max = function CAst.make @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; - observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) + observe_tclTHENLIST (fun _ _ -> str "make_rewrite_list")[ (* x < S max proof *) Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm)); - observe_tac (str "prove_le(2)") prove_le + observe_tac (fun _ _ -> str "prove_le(2)") prove_le ] ] ) let make_rewrite expr_info l hp max = tclTHENFIRST - (observe_tac (str "make_rewrite") (make_rewrite_list expr_info max l)) - (observe_tac (str "make_rewrite") (tclTHENS + (observe_tac (fun _ _ -> str "make_rewrite") (make_rewrite_list expr_info max l)) + (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS (fun g -> let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in @@ -905,30 +909,30 @@ let make_rewrite expr_info l hp max = let def_na,_,_ = destProd sigma t in Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name in - observe_tac (str "general_rewrite_bindings") + observe_tac (fun _ _ -> str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g) - [observe_tac(str "make_rewrite finalize") ( + [observe_tac(fun _ _ -> str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) - (observe_tclTHENLIST (str "make_rewrite")[ + (observe_tclTHENLIST (fun _ _ -> str "make_rewrite")[ Proofview.V82.of_tactic (simpl_iter Locusops.onConcl); - observe_tac (str "unfold functional") + observe_tac (fun _ _ -> str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference expr_info.func)])); (list_rewrite true (List.map (fun e -> mkVar e,true) expr_info.eqs)); - (observe_tac (str "h_reflexivity") + (observe_tac (fun _ _ -> str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity) ) ])) ; - observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *) + observe_tclTHENLIST (fun _ _ -> str "make_rewrite1")[ (* x < S (S max) proof *) Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS))); - observe_tac (str "prove_le (3)") prove_le + observe_tac (fun _ _ -> str "prove_le (3)") prove_le ] ]) ) @@ -937,7 +941,7 @@ let rec compute_max rew_tac max l = match l with | [] -> rew_tac max | (_,p,_)::l -> - observe_tclTHENLIST (str "compute_max")[ + observe_tclTHENLIST (fun _ _ -> str "compute_max")[ Proofview.V82.of_tactic (simplest_elim (mkApp(delayed_force max_constr, [| max; mkVar p|]))); tclDO 3 (Proofview.V82.of_tactic intro); @@ -954,17 +958,17 @@ let rec destruct_hex expr_info acc l = match List.rev acc with | [] -> tclIDTAC | (_,p,hp)::tl -> - observe_tac (str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) + observe_tac (fun _ _ -> str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) end | (v,hex)::l -> - observe_tclTHENLIST (str "destruct_hex")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_hex")[ Proofview.V82.of_tactic (simplest_case (mkVar hex)); Proofview.V82.of_tactic (clear [hex]); tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hp -> onNthHypId 2 (fun p -> observe_tac - (str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) + (fun _ _ -> str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) (destruct_hex expr_info ((v,p,hp)::acc) l) ) ) @@ -972,7 +976,7 @@ let rec destruct_hex expr_info acc l = let rec intros_values_eq expr_info acc = tclORELSE( - observe_tclTHENLIST (str "intros_values_eq")[ + observe_tclTHENLIST (fun _ _ -> str "intros_values_eq")[ tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hex -> (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc))) @@ -983,23 +987,17 @@ let rec intros_values_eq expr_info acc = )) let equation_others _ expr_info continuation_tac infos = - fun g -> - let env = pf_env g in - let sigma = project g in if expr_info.is_final && expr_info.is_main_branch then - observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info) + observe_tac (fun env sigma -> str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (tclTHEN (continuation_tac infos) - (fun g -> - let env = pf_env g in - let sigma = project g in - observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []) g)) g - else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) g + (observe_tac (fun env sigma -> str "intros_values_eq equation_others " ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (fun env sigma -> str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch - then ((observe_tac (str "intros_values_eq equation_app") (intros_values_eq expr_info []))) + then ((observe_tac (fun _ _ -> str "intros_values_eq equation_app") (intros_values_eq expr_info []))) else continuation_tac infos let equation_app_rec (f,args) expr_info continuation_tac info g = @@ -1008,19 +1006,19 @@ let equation_app_rec (f,args) expr_info continuation_tac info g = try let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in - observe_tac (str "app_rec found") (continuation_tac new_infos) g + observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) g with Not_found -> if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "equation_app_rec") + observe_tclTHENLIST (fun _ _ -> str "equation_app_rec") [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}; - observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info []) + observe_tac (fun _ _ -> str "app_rec intros_values_eq") (intros_values_eq expr_info []) ] g else - observe_tclTHENLIST (str "equation_app_rec1")[ + observe_tclTHENLIST (fun _ _ -> str "equation_app_rec1")[ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); - observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}) + observe_tac (fun _ _ -> str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}) ] g end @@ -1104,7 +1102,7 @@ let termination_proof_header is_mes input_type ids args_id relation (h_intros args_id) (tclTHENS (observe_tac - (str "first assert") + (fun _ _ -> str "first assert") (Proofview.V82.of_tactic (assert_before (Name wf_rec_arg) (mkApp (delayed_force acc_rel, @@ -1116,7 +1114,7 @@ let termination_proof_header is_mes input_type ids args_id relation (* accesibility proof *) tclTHENS (observe_tac - (str "second assert") + (fun _ _ -> str "second assert") (Proofview.V82.of_tactic (assert_before (Name wf_thm) (mkApp (delayed_force well_founded,[|input_type;relation|])) @@ -1124,26 +1122,26 @@ let termination_proof_header is_mes input_type ids args_id relation ) [ (* interactive proof that the relation is well_founded *) - observe_tac (str "wf_tac") (wf_tac is_mes (Some args_id)); + observe_tac (fun _ _ -> str "wf_tac") (wf_tac is_mes (Some args_id)); (* this gives the accessibility argument *) observe_tac - (str "apply wf_thm") + (fun _ _ -> str "apply wf_thm") (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))) ) ] ; (* rest of the proof *) - observe_tclTHENLIST (str "rest of proof") - [observe_tac (str "generalize") + observe_tclTHENLIST (fun _ _ -> str "rest of proof") + [observe_tac (fun _ _ -> str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); + observe_tac (fun _ _ -> str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); h_intros args_id; Proofview.V82.of_tactic (Simple.intro wf_rec_arg); - observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) + observe_tac (fun _ _ -> str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ] ) g @@ -1222,8 +1220,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a g end -let get_current_subgoals_types () = - let p = Proof_global.give_me_the_proof () in +let get_current_subgoals_types pstate = + let p = Proof_global.give_me_the_proof pstate in let sgs,_,_,_,sigma = Proof.proof p in sigma, List.map (Goal.V82.abstract_type sigma) sgs @@ -1283,8 +1281,8 @@ let clear_goals sigma = List.map clear_goal -let build_new_goal_type () = - let sigma, sub_gls_types = get_current_subgoals_types () in +let build_new_goal_type pstate = + let sigma, sub_gls_types = get_current_subgoals_types pstate in (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let sub_gls_types = clear_goals sigma sub_gls_types in (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) @@ -1299,9 +1297,9 @@ let is_opaque_constant c = | Declarations.Def _ -> Proof_global.Transparent | Declarations.Primitive _ -> Proof_global.Opaque -let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = +let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = Proof_global.get_current_proof_name () in + let current_proof_name = Proof_global.get_current_proof_name pstate in let name = match goal_name with | Some s -> s | None -> @@ -1325,11 +1323,10 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in - Proof_global.discard_all (); - build_proof (Evd.from_env env) + let pstate = build_proof env (Evd.from_env env) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in - observe_tclTHENLIST (str "") + observe_tclTHENLIST (fun _ _ -> str "") [ Proofview.V82.of_tactic (generalize [lemma]); Proofview.V82.of_tactic (Simple.intro hid); @@ -1353,7 +1350,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g | _ -> incr h_num; - (observe_tac (str "finishing using") + (observe_tac (fun _ _ -> str "finishing using") ( tclCOMPLETE( tclFIRST[ @@ -1369,20 +1366,19 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ) ) g) -; - Lemmas.save_proof (Vernacexpr.Proved(opacity,None)); + in + let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in + () in - Lemmas.start_proof + let pstate = Lemmas.start_proof ~ontop:(Some pstate) na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) - sigma gls_type - ~hook:(Lemmas.mk_hook hook); - if Indfun_common.is_strict_tcc () + sigma gls_type ~hook:(Lemmas.mk_hook hook) in + let pstate = if Indfun_common.is_strict_tcc () then - ignore (by (Proofview.V82.tactic (tclIDTAC))) + fst @@ by (Proofview.V82.tactic (tclIDTAC)) pstate else - begin - ignore (by (Proofview.V82.tactic begin + fst @@ by (Proofview.V82.tactic begin fun g -> tclTHEN (decompose_and_tac) @@ -1398,14 +1394,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ) using_lemmas) ) tclIDTAC) - g end)) - end; + g end) pstate + in try - ignore (by (Proofview.V82.tactic tclIDTAC)); (* raises UserError _ if the proof is complete *) + Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *) with UserError _ -> - defined () - - + defined pstate let com_terminate tcc_lemma_name @@ -1418,32 +1412,26 @@ let com_terminate thm_name using_lemmas nb_args ctx hook = - let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evd, env = Pfedit.get_current_context () in (* XXX *) - Lemmas.start_proof thm_name + let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = + let pstate = Lemmas.start_proof ~ontop:None thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook; - - ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); - ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref - input_type relation rec_arg_num )))) + ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in + let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in + fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num ))) pstate in - start_proof ctx tclIDTAC tclIDTAC; + let pstate = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in try - let sigma, new_goal_type = build_new_goal_type () in + let sigma, new_goal_type = build_new_goal_type pstate in let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in - open_new_goal start_proof sigma + open_new_goal pstate start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) - (new_goal_type); + (new_goal_type) with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined () - - - - + defined pstate let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1453,33 +1441,27 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t) let terminate_constr = EConstr.of_constr terminate_constr in let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in let x = n_x_id ids nargs in - observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ + observe_tac (fun _ _ -> str "start_equation") (observe_tclTHENLIST (fun _ _ -> str "start_equation") [ h_intros x; Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]); - observe_tac (str "simplest_case") + observe_tac (fun _ _ -> str "simplest_case") (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))); - observe_tac (str "prove_eq") (cont_tactic x)]) g;; + observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x)]) g;; -let (com_eqn : int -> Id.t -> - GlobRef.t -> GlobRef.t -> GlobRef.t - -> Constr.t -> unit) = - fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> +let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type = let open CVars in let opacity = match terminate_ref with | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evd, env = Pfedit.get_current_context () in (* XXX *) - let evd = Evd.from_ctx (Evd.evar_universe_context evd) in + let evd = Evd.from_ctx uctx in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - (Lemmas.start_proof eq_name (Global, false, Proof Lemma) - ~sign:(Environ.named_context_val env) - evd - (EConstr.of_constr equation_lemma_type); - ignore (by + let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd + (EConstr.of_constr equation_lemma_type) in + let pstate = fst @@ by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> prove_eq (fun _ -> tclIDTAC) @@ -1506,15 +1488,16 @@ let (com_eqn : int -> Id.t -> ih = Id.of_string "______"; } ) - ))); + )) pstate in (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) (* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) - Flags.silently (fun () -> Lemmas.save_proof (Vernacexpr.Proved(opacity,None))) () ; -(* Pp.msgnl (str "eqn finished"); *) - );; + let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in + () +(* Pp.msgnl (fun _ _ -> str "eqn finished"); *) + let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq - generate_induction_principle using_lemmas : unit = + generate_induction_principle using_lemmas : Proof_global.t option = let open Term in let open Constr in let open CVars in @@ -1529,15 +1512,15 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in - (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) + (* Pp.msgnl (fun _ _ -> str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in let eq' = EConstr.Unsafe.to_constr eq' in let res = -(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) -(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) -(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) +(* Pp.msgnl (fun _ _ -> str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) +(* Pp.msgnl (fun _ _ -> str "rec_arg_num := " ++ str (fun _ _ -> string_of_int rec_arg_num)); *) +(* Pp.msgnl (fun _ _ -> str "eq' := " ++ str (fun _ _ -> string_of_int rec_arg_num)); *) match Constr.kind eq' with | App(e,[|_;_;eq_fix|]) -> mkLambda (make_annot (Name function_name) Sorts.Relevant,function_type,subst_var function_name (compose_lam res_vars eq_fix)) @@ -1562,14 +1545,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in - (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook _ _ _ _ = + (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) + let hook uctx _ _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) - let stop = - try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); + let stop = + (* XXX: What is the correct way to get sign at hook time *) + let sign = Environ.named_context_val Global.(env ()) in + try com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); false with e when CErrors.noncritical e -> begin @@ -1601,14 +1586,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num in (* XXX STATE Why do we need this... why is the toplevel protection not enought *) funind_purify (fun () -> - com_terminate - tcc_lemma_name - tcc_lemma_constr - is_mes functional_ref - (EConstr.of_constr rec_arg_type) - relation rec_arg_num - term_id - using_lemmas - (List.length res_vars) - evd (Lemmas.mk_hook hook)) - () + let pstate = com_terminate + tcc_lemma_name + tcc_lemma_constr + is_mes functional_ref + (EConstr.of_constr rec_arg_type) + relation rec_arg_num + term_id + using_lemmas + (List.length res_vars) + evd (Lemmas.mk_hook hook) + in pstate) () diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 549f1fc0e4..a006c2c354 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,6 +14,6 @@ bool -> int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0428f08138..f5098d2a34 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -53,6 +53,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } in let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -348,6 +349,7 @@ let constr_flags () = { Pretyping.fail_evar = false; Pretyping.expand_evars = true; Pretyping.program_mode = false; + Pretyping.polymorphic = false; } let refine_tac ist simple with_classes c = @@ -813,9 +815,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; } END (* ********************************************************************* *) @@ -913,9 +915,9 @@ END the semantics of the LCF-style tactics, hence with the classic tactic mode. *) VERNAC COMMAND EXTEND GrabEvars -| [ "Grab" "Existential" "Variables" ] +| ![ proof ] [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } END (* Shelves all the goals under focus. *) @@ -945,9 +947,9 @@ END (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve -| [ "Unshelve" ] +| ![ proof ] [ "Unshelve" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -1098,8 +1100,8 @@ END VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { Proof_global.compact_the_proof () } +| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> + { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 3a4b0571d4..523c7c8305 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -58,6 +58,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } in let map c env sigma = c env sigma in List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index a348e2cea4..7eb34158e8 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -374,20 +374,21 @@ let () = declare_int_option { optwrite = fun n -> print_info_trace := n; } -let vernac_solve n info tcom b = +let vernac_solve ~pstate n info tcom b = let open Goal_select in - let status = Proof_global.with_current_proof (fun etac p -> - let with_end_tac = if b then Some etac else None in - let global = match n with SelectAll | SelectList _ -> true | _ -> false in - let info = Option.append info !print_info_trace in - let (p,status) = - Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p - in - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - let p = Proof.maximal_unfocus Vernacentries.command_focus p in - p,status) in - if not status then Feedback.feedback Feedback.AddedAxiom + let pstate, status = Proof_global.with_current_proof (fun etac p -> + let with_end_tac = if b then Some etac else None in + let global = match n with SelectAll | SelectList _ -> true | _ -> false in + let info = Option.append info !print_info_trace in + let (p,status) = + Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p + in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p,status) pstate in + if not status then Feedback.feedback Feedback.AddedAxiom; + Some pstate let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s @@ -434,12 +435,12 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false } VERNAC { tactic_mode } EXTEND VernacSolve -| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - vernac_solve g n t def + Vernacentries.vernac_require_open_proof vernac_solve g n t def } -| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in @@ -449,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve VtLater } -> { let t = rm_abstract t in - vernac_solve Goal_select.SelectAll n t def + Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index a12dee48a8..de3a9c9fa9 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram open Obligations -let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac +let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac) +let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac) let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| [ "Obligation" integer(num) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 86a227415a..469551809c 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None None (Some lemma3) } END @@ -234,64 +234,64 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid atts [] a aeq t n; + add_setoid atts [] a aeq t n } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid atts binders a aeq t n; + add_setoid atts binders a aeq t n } - | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => { VtUnknown, VtNow } -> { - add_morphism_infer atts m n; + add_morphism_infer atts m n } - | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { - add_morphism atts [] m s n; + add_morphism atts [] m s n } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { - add_morphism atts binders m s n; + add_morphism atts binders m s n } END @@ -310,7 +310,12 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY -| [ "Print" "Rewrite" "HintDb" preident(s) ] -> - { let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) } +| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { (* This command should not use the proof env, keeping previous + behavior as requested in review. *) + fun ~pstate -> + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s); + pstate } END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 1bdba699f7..80070a7493 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1307,7 +1307,6 @@ let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) let register_basic_print0 wit f g h = Genprint.register_print0 wit (lift f) (lift g) (lift_top h) - let pr_glob_constr_pptac env sigma c = pr_glob_constr_env env c diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b1d5c0252f..75565c1a34 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -618,7 +618,9 @@ let solve_remaining_by env sigma holes by = in (* Only solve independent holes *) let indep = List.map_filter map holes in - let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in + let ist = { Geninterp.lfun = Id.Map.empty + ; poly = false + ; extra = Geninterp.TacStore.empty } in let solve_tac = match tac with | Genarg.GenArg (Genarg.Glbwit tag, tac) -> Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ()) @@ -1790,15 +1792,15 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance atts binders instance fields = +let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in - new_instance ~program_mode atts.polymorphic + new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info -let declare_instance_refl atts binders a aeq n lemma = +let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" - in anew_instance atts binders instance + in anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym atts binders a aeq n lemma = @@ -1811,47 +1813,44 @@ let declare_instance_trans atts binders a aeq n lemma = in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "transitivity"),lemma)] -let declare_relation atts ?(binders=[]) a aeq n refl symm trans = +let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" - in ignore(anew_instance atts binders instance []); + let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in + let _, pstate = anew_instance ~pstate atts binders instance [] in match (refl,symm,trans) with - (None, None, None) -> () + (None, None, None) -> pstate | (Some lemma1, None, None) -> - ignore (declare_instance_refl atts binders a aeq n lemma1) + snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1 | (None, Some lemma2, None) -> - ignore (declare_instance_sym atts binders a aeq n lemma2) + snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 | (None, None, Some lemma3) -> - ignore (declare_instance_trans atts binders a aeq n lemma3) + snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3 | (Some lemma1, Some lemma2, None) -> - ignore (declare_instance_refl atts binders a aeq n lemma1); - ignore (declare_instance_sym atts binders a aeq n lemma2) + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 | (Some lemma1, None, Some lemma3) -> - let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" - in ignore( - anew_instance atts binders instance + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] | (None, Some lemma2, Some lemma3) -> - let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" - in ignore( - anew_instance atts binders instance + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] | (Some lemma1, Some lemma2, Some lemma3) -> - let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in - let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" - in ignore( - anew_instance atts binders instance + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1947,18 +1946,18 @@ let warn_add_setoid_deprecated = CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) -let add_setoid atts binders a aeq t n = +let add_setoid ~pstate atts binders a aeq t n = warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); - let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" - in ignore( - anew_instance atts binders instance + in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] let make_tactic name = @@ -1970,7 +1969,7 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer atts m n = +let add_morphism_infer ~pstate atts m n : Proof_global.t option = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); (* NB: atts.program is ignored, program mode automatically set by vernacentries *) @@ -1981,45 +1980,47 @@ let add_morphism_infer atts m n = if Lib.is_modtype () then let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id - (Entries.ParameterEntry - (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry + (None,(instance,uctx),None), + Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) + add_instance (Typeclasses.new_instance + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); + declare_projection n instance_id (ConstRef cst); + pstate else let kind = Decl_kinds.Global, atts.polymorphic, - Decl_kinds.DefinitionBody Decl_kinds.Instance + Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ _ _ = function - | Globnames.ConstRef cst -> - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info + | Globnames.ConstRef cst -> + add_instance (Typeclasses.new_instance + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) - | _ -> assert false + declare_projection n instance_id (ConstRef cst) + | _ -> assert false in let hook = Lemmas.mk_hook hook in - Flags.silently - (fun () -> - Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance); - ignore (Pfedit.by (Tacinterp.interp tac))) () + Flags.silently + (fun () -> + let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () -let add_morphism atts binders m s n = +let add_morphism ~pstate atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance + None + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in + pstate (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 2457b265f0..a200cb5ced 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -81,18 +81,18 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : rewrite_attributes -> +val declare_relation : pstate:Proof_global.t option -> rewrite_attributes -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> - constr_expr option -> constr_expr option -> constr_expr option -> unit + constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option -val add_setoid : +val add_setoid : pstate:Proof_global.t option -> rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> - Id.t -> unit + Id.t -> Proof_global.t option -val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit +val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option -val add_morphism : - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit +val add_morphism : pstate:Proof_global.t option -> + rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index eac84f0543..4398fb14ab 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -138,9 +138,10 @@ let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () (* Signature for interpretation: val_interp and interpretation functions *) -type interp_sign = Geninterp.interp_sign = { - lfun : value Id.Map.t; - extra : TacStore.t } +type interp_sign = Geninterp.interp_sign = + { lfun : value Id.Map.t + ; poly : bool + ; extra : TacStore.t } let extract_trace ist = if is_traced () then match TacStore.get ist.extra f_trace with @@ -544,12 +545,7 @@ let interp_gen kind ist pattern_mode flags env sigma c = let (_, dummy_proofview) = Proofview.init sigma [] in (* Again this is called at times with no open proof! *) - let name, poly = - try - let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in - name, poly - with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false - in + let name, poly = Id.of_string "tacinterp", ist.poly in let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) term @@ -566,11 +562,13 @@ let constr_flags () = { fail_evar = true; expand_evars = true; program_mode = false; + polymorphic = false; } (* Interprets a constr; expects evars to be solved *) let interp_constr_gen kind ist env sigma c = - interp_gen kind ist false (constr_flags ()) env sigma c + let flags = { (constr_flags ()) with polymorphic = ist.Geninterp.poly } in + interp_gen kind ist false flags env sigma c let interp_constr = interp_constr_gen WithoutTypeConstraint @@ -582,6 +580,7 @@ let open_constr_use_classes_flags () = { fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } let open_constr_no_classes_flags () = { @@ -590,6 +589,7 @@ let open_constr_no_classes_flags () = { fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } let pure_open_constr_flags = { @@ -598,6 +598,7 @@ let pure_open_constr_flags = { fail_evar = false; expand_evars = false; program_mode = false; + polymorphic = false; } (* Interprets an open constr *) @@ -1021,6 +1022,7 @@ let type_uconstr ?(flags = (constr_flags ())) ltac_idents = closure.idents; ltac_genargs = Id.Map.empty; } in + let flags = { flags with polymorphic = ist.Geninterp.poly } in understand_ltac flags env sigma vars expected_type term end @@ -1146,6 +1148,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (* For extensions *) | TacAlias {loc; v=(s,l)} -> let alias = Tacenv.interp_alias s in + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = @@ -1153,8 +1156,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { - lfun = lfun; - extra = TacStore.set ist.extra f_trace trace; } in + lfun + ; poly + ; extra = TacStore.set ist.extra f_trace trace } in val_interp ist alias.Tacenv.alias_body >>= fun v -> Ftactic.lift (tactic_of_value ist v) in @@ -1207,12 +1211,13 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let ids = extract_ids [] ist.lfun Id.Set.empty in let loc_info = (Option.default loc loc',LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in push_trace loc_info ist >>= fun trace -> let extra = TacStore.set extra f_trace trace in - let ist = { lfun = Id.Map.empty; extra = extra; } in + let ist = { lfun = Id.Map.empty; poly; extra } in let appl = GlbAppl[r,[]] in Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false (val_interp ~appl ist (Tacenv.interp_ltac r)) @@ -1260,6 +1265,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t = (* Interprets an application node *) and interp_app loc ist fv largs : Val.t Ftactic.t = + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in if has_type fv (topwit wit_tacvalue) then @@ -1277,9 +1283,11 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = if List.is_empty lvar then begin wrap_error begin - let ist = { - lfun = newlfun; - extra = TacStore.set ist.extra f_trace []; } in + let ist = + { lfun = newlfun + ; poly + ; extra = TacStore.set ist.extra f_trace [] + } in Profile_ltac.do_profile "interp_app" trace ~count_call:false (catch_error_tac trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) @@ -1317,8 +1325,10 @@ and tactic_of_value ist vle = if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl,trace,lfun,[],t) -> + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let ist = { lfun = lfun; + poly; extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) @@ -1388,6 +1398,7 @@ and interp_letin ist llc u = (** [interp_match_success lz ist succ] interprets a single matching success (of type {!Tactic_matching.t}). *) and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in let lctxt = Id.Map.map interp_context context in let hyp_subst = Id.Map.map Value.of_constr terms in @@ -1396,9 +1407,11 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = val_interp ist lhs >>= fun v -> if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (appl,trace,lfun,[],t) -> - let ist = { - lfun = lfun; - extra = TacStore.set ist.extra f_trace trace; } in + let ist = + { lfun = lfun + ; poly + ; extra = TacStore.set ist.extra f_trace trace + } in let tac = eval_tactic ist t in let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy)) @@ -1872,7 +1885,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let default_ist () = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in - { lfun = Id.Map.empty; extra = extra } + { lfun = Id.Map.empty; poly = false; extra = extra } let eval_tactic t = Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *) @@ -1912,11 +1925,12 @@ end let interp_tac_gen lfun avoid_ids debug t = + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in - let ist = { lfun = lfun; extra = extra } in + let ist = { lfun; poly; extra } in let ltacvars = Id.Map.domain lfun in interp_tactic ist (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) @@ -2057,20 +2071,15 @@ let interp_redexp env sigma r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let eval lfun env sigma ty tac = + let eval lfun poly env sigma ty tac = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in - let ist = { lfun = lfun; extra; } in + let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* XXX: This depends on the global state which is bad; the hooking - mechanism should be modified. *) - let name, poly = - try - let (_, poly, _) = Proof_global.get_current_persistence () in - let name = Proof_global.get_current_proof_name () in - name, poly - with | Proof_global.NoCurrentProof -> - Id.of_string "ltac_gen", false - in + (* EJGA: We sould also pass the proof name if desired, for now + poly seems like enough to get reasonable behavior in practice + *) + let name, poly = Id.of_string "ltac_gen", poly in + let name, poly = Id.of_string "ltac_gen", poly in let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index d9c80bb835..22a092fa8b 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -39,9 +39,10 @@ module TacStore : Store.S with and type 'a field = 'a Geninterp.TacStore.field (** Signature for interpretation: val\_interp and interpretation functions *) -type interp_sign = Geninterp.interp_sign = { - lfun : value Id.Map.t; - extra : TacStore.t } +type interp_sign = Geninterp.interp_sign = + { lfun : value Id.Map.t + ; poly : bool + ; extra : TacStore.t } open Genintern diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 52a83a038f..04f3116664 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -370,7 +370,10 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - let sigma, env = Pfedit.get_current_context () in + (* XXX: This hooks into the ExplainErr extension API + so it is tricky to provide the right env for now. *) + let env = Global.env () in + let sigma = Evd.from_env env in Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7db47e13a5..6c04fe9a8a 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -877,9 +877,9 @@ struct * This is the big generic function for expression parsers. *) - let parse_expr cenv sigma parse_constant parse_exp ops_spec env term = + let parse_expr env sigma parse_constant parse_exp ops_spec term_env term = if debug - then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env cenv sigma term); + then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term); (* let constant_or_variable env term = @@ -928,7 +928,7 @@ struct | _ -> parse_variable env term ) | _ -> parse_variable env term in - parse_expr env term + parse_expr term_env term let zop_spec = [ @@ -1007,7 +1007,7 @@ struct res - let parse_zexpr env sigma = parse_expr env sigma + let parse_zexpr env sigma = parse_expr env sigma (zconstant sigma) (fun expr x -> let exp = (parse_z sigma x) in @@ -1038,16 +1038,17 @@ struct Mc.PEpow(expr,exp)) rop_spec - let parse_arith parse_op parse_expr env cstr gl = + let parse_arith parse_op parse_expr term_env cstr gl = let sigma = gl.sigma in + let env = gl.env in if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env env sigma cstr ++ fnl ()); match EConstr.kind sigma cstr with | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in - let (e1,env) = parse_expr gl.env sigma env lhs in - let (e2,env) = parse_expr gl.env sigma env rhs in - ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env) + let (e1,term_env) = parse_expr env sigma term_env lhs in + let (e2,term_env) = parse_expr env sigma term_env rhs in + ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},term_env) | _ -> failwith "error : parse_arith(2)" let parse_zarith = parse_arith parse_zop parse_zexpr diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index 3ce6478700..6be556b2ae 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -86,15 +86,20 @@ END VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_theory id t l } - | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { + | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { + fun ~pstate -> Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> - let sigma, env = Pfedit.get_current_context () in + (* We should use the global env here as this shouldn't contain proof + data, however preserving behavior as requested in review. *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) - ) !from_name } + ) !from_name; + pstate } END TACTIC EXTEND ring_lookup @@ -130,15 +135,20 @@ END VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_field_theory id t l } -| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { +| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { + fun ~pstate -> Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> - let sigma, env = Pfedit.get_current_context () in + (* We should use the global env here as this shouldn't + contain proof data. *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) - ) !field_from_name } + ) !field_from_name; + pstate } END TACTIC EXTEND field_lookup diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 6956120a6a..2a84469af0 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -246,6 +246,7 @@ let interp_refine ist gl rc = fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in @@ -1175,7 +1176,7 @@ let genstac (gens, clr) = tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens) let gen_tmp_ids - ?(ist=Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty })) gl + ?(ist=Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })) gl = let gl, ctx = pull_ctx gl in push_ctxs ctx @@ -1232,7 +1233,7 @@ let abs_wgen keep_let f gen (gl,args,c) = let evar_closed t p = if occur_existential sigma t then CErrors.user_err ?loc:(loc_of_cpattern p) ~hdr:"ssreflect" - (pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ + (pr_econstr_pat env sigma t ++ str" contains holes and matches no subterm of the goal") in match gen with | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 94f7d24242..350bb9019e 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -239,8 +239,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let elimty = Reductionops.whd_all env (project gl) elimty in seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl in - ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elim))); - ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elimty))); + let () = + let sigma = project gl in + ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); + ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) | _ -> assert false in @@ -304,7 +306,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = * looking at the ones provided by the user and the inferred ones looking at * the type of the elimination principle *) let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern env p) in - let pp_inf_pat gl (_,_,t,_) = pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl t)) in + let pp_inf_pat gl (_,_,t,_) = pr_econstr_pat env (project gl) (fire_subst gl t) in let patterns, clr, gl = let rec loop patterns clr i = function | [],[] -> patterns, clr, gl @@ -318,7 +320,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr c))); + ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in @@ -341,7 +343,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let elim_pred, gen_eq_tac, clr, gl = let error gl t inf_t = errorstrm Pp.(str"The given pattern matches the term"++ spc()++pp_term gl t++spc()++str"while the inferred pattern"++ - spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in + spc()++pr_econstr_pat env (project gl) (fire_subst gl inf_t)++spc()++ str"doesn't") in let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) = let p = unif_redex gl p inf_t in if is_undef_pat p then @@ -426,7 +428,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = if not (Evar.Set.is_empty inter) then begin let i = Evar.Set.choose inter in let pat = List.find (fun t -> Evar.Set.mem i (evars_of_term t)) patterns in - errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr pat)++spc()++ + errorstrm Pp.(str"Pattern"++spc()++pr_econstr_pat env (project gl) pat++spc()++ str"was not completely instantiated and one of its variables"++spc()++ str"occurs in the type of another non-instantiated pattern variable"); end diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 902098c8ce..5abbc214de 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -205,7 +205,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with | App (c', _) -> get_evalref env sigma c' | Cast (c', _, _) -> get_evalref env sigma c' | Proj(c,_) -> EvalConstRef(Projection.constant c) - | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable") + | _ -> errorstrm Pp.(str "The term " ++ pr_econstr_pat (Global.env ()) sigma c ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with @@ -244,7 +244,7 @@ let unfoldintac occ rdx t (kt,_) gl = try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " - ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), + ++ pr_econstr_pat env sigma0 t ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") @@ -270,12 +270,12 @@ let unfoldintac occ rdx t (kt,_) gl = else try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t) with _ -> errorstrm Pp.(str "The term " ++ - pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))), + pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_econstr_pat env sigma t)), fake_pmatcher_end in let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) - with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat env0 sigma (EConstr.Unsafe.to_constr t)) in + with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in let _ = conclude () in Proofview.V82.of_tactic (convert_concl concl) gl ;; @@ -415,7 +415,7 @@ let rwcltac cl rdx dir sr gl = let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> - errorstrm Pp.(str "no cast from " ++ pr_constr_pat (pf_env gl) (project gl) (EConstr.Unsafe.to_constr (snd sr)) + errorstrm Pp.(str "no cast from " ++ pr_econstr_pat (pf_env gl) (project gl) (snd sr) ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in @@ -433,9 +433,8 @@ let rwcltac cl rdx dir sr gl = if occur_existential (project gl) (Tacmach.pf_concl gl) then errorstrm Pp.(str "Rewriting impacts evars" ++ error) else errorstrm Pp.(str "Dependent type error in rewrite of " - ++ pr_constr_env (pf_env gl) (project gl) - (Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant) - (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl)) + ++ pr_econstr_env (pf_env gl) (project gl) + (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl) ++ error) in tclTHEN cvtac' rwtac gl @@ -480,7 +479,7 @@ let rwprocess_rule dir rule gl = let t = if red = 1 then Tacred.hnf_constr env sigma t0 else Reductionops.whd_betaiotazeta sigma t0 in - ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))); + ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> let sigma = Evd.create_evar_defs sigma in @@ -539,8 +538,8 @@ let rwprocess_rule dir rule gl = sigma, (d, r', lhs, rhs) :: rs | _ -> if red = 0 then loop d sigma r t rs 1 - else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) - ++ spc() ++ str "in rule " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr (snd rule))) + else errorstrm Pp.(str "not a rewritable relation: " ++ pr_econstr_pat env sigma t + ++ spc() ++ str "in rule " ++ pr_econstr_pat env sigma (snd rule)) in let sigma, r = rule in let t = Retyping.get_type_of env sigma r in @@ -554,9 +553,9 @@ let rwrxtac occ rdx_pat dir rule gl = let find_rule rdx = let rec rwtac = function | [] -> - errorstrm Pp.(str "pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr rdx) ++ + errorstrm Pp.(str "pattern " ++ pr_econstr_pat env (project gl) rdx ++ str " does not match " ++ pr_dir_side dir ++ - str " of " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (snd rule))) + str " of " ++ pr_econstr_pat env (project gl) (snd rule)) | (d, r, lhs, rhs) :: rs -> try let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index be9586fdd7..3cadc92bcc 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -50,7 +50,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++ - pr_constr_pat env sigma (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++ + pr_econstr_pat env sigma c++spc()++str"did not match and has holes."++spc()++ str"Did you mean pose?") else let c, (gl, cty) = match EConstr.kind sigma c with | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index d3f89147fa..0a0d9b12fa 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -566,17 +566,21 @@ let print_view_hints env sigma kind l = } VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY -| [ "Print" "Hint" "View" ssrviewpos(i) ] -> +| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] -> { - let sigma, env = Pfedit.get_current_context () in - match i with + fun ~pstate -> + (* XXX this is incorrect *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + (match i with | Some k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k) | None -> List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k)) [ Ssrview.AdaptorDb.Forward; Ssrview.AdaptorDb.Backward; - Ssrview.AdaptorDb.Equivalence ] + Ssrview.AdaptorDb.Equivalence ]); + pstate } END diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 5eb106cc26..1deb935d5c 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -373,6 +373,12 @@ let pr_constr_pat env sigma c0 = if isEvar c then hole_var else map wipe_evar c in pr_constr_env env sigma (wipe_evar c0) +let ehole_var = EConstr.mkVar (Id.of_string "_") +let pr_econstr_pat env sigma c0 = + let rec wipe_evar c = let open EConstr in + if isEvar sigma c then ehole_var else map sigma wipe_evar c in + pr_econstr_env env sigma (wipe_evar c0) + (* Turn (new) evars into metas *) let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = let ise = ref ise0 in @@ -694,8 +700,7 @@ let source env = match upats_origin, upats with (if fixed_upat ise p then str"term " else str"partial term ") ++ pr_constr_pat env ise (p2t p) ++ spc() | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ - pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++ - pr_constr_pat env ise (p2t p) ++ fnl() + pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++ pr_constr_pat env ise (p2t p) ++ fnl() | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ pr_constr_pat env ise rule ++ spc() | _, [] | None, _::_::_ -> @@ -732,13 +737,13 @@ let rec uniquize = function env, 0, uniquize (instances ()) | NoMatch when (not raise_NoMatch) -> if !failed_because_of_TC then - errorstrm (source env++strbrk"matches but type classes inference fails") + errorstrm (source env ++ strbrk"matches but type classes inference fails") else errorstrm (source env ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> let dir = match upats_origin with Some (d,_) -> d | _ -> CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in - errorstrm (str"all matches of "++source env++ + errorstrm (str"all matches of "++ source env ++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); let sigma, _, ({up_f = pf; up_a = pa} as u) = @@ -823,7 +828,7 @@ let pr_pattern_aux pr_constr = function | E_As_X_In_T (e,x,t) -> pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t let pp_pattern env (sigma, p) = - pr_pattern_aux (fun t -> pr_constr_pat env sigma (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p + pr_pattern_aux (fun t -> pr_econstr_pat env sigma (pi3 (nf_open_term sigma sigma (EConstr.of_constr t)))) p let pr_cpattern = pr_term let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern) @@ -1253,10 +1258,8 @@ let fill_occ_term env cl occ sigma0 (sigma, t) = if sigma' != sigma0 then raise NoMatch else cl, (Evd.merge_universe_context sigma' uc, t') with _ -> - errorstrm (str "partial term " ++ - pr_constr_pat env sigma - (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) ++ - str " does not match any subterm of the goal") + errorstrm (str "partial term " ++ pr_econstr_pat env sigma t + ++ str " does not match any subterm of the goal") let pf_fill_occ_term gl occ t = let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in @@ -1264,7 +1267,7 @@ let pf_fill_occ_term gl occ t = cl, t let cpattern_of_id id = - ' ', (DAst.make @@ GRef (VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty }) + ' ', (DAst.make @@ GRef (VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty }) let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with | _, Some { CAst.v = CHole _ } | GHole _, None -> true diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 1143bcc813..25975c84e8 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -223,6 +223,7 @@ val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.Id.t -> cpattern val pr_constr_pat : env -> evar_map -> constr -> Pp.t +val pr_econstr_pat : env -> evar_map -> econstr -> Pp.t val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 73a2b99434..baa4ae0306 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -35,8 +35,23 @@ ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { let (sigma, env) = Pfedit.get_current_context () in - vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + + { (* It is a bug to use the proof context here, but at the request of + * the reviewers we keep this broken behavior for now. The Global env + * should be used instead, and the `env, sigma` parameteter to the + * numeral notation command removed. + *) + fun ~pstate -> + let sigma, env = match pstate with + | None -> + let env = Global.env () in + let sigma = Evd.from_env env in + sigma, env + | Some pstate -> + Pfedit.get_current_context pstate + in + vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o; + pstate } END diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg index 171e0e213d..cc8c13a84b 100644 --- a/plugins/syntax/g_string.mlg +++ b/plugins/syntax/g_string.mlg @@ -19,8 +19,22 @@ open Stdarg } VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) ] -> - { let (sigma, env) = Pfedit.get_current_context () in - vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) } + { (* It is a bug to use the proof context here, but at the request of + * the reviewers we keep this broken behavior for now. The Global env + * should be used instead, and the `env, sigma` parameteter to the + * numeral notation command removed. + *) + fun ~pstate -> + let sigma, env = match pstate with + | None -> + let env = Global.env () in + let sigma = Evd.from_env env in + sigma, env + | Some pstate -> + Pfedit.get_current_context pstate + in + vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc); + pstate } END |