diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 25 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 11 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 2 |
3 files changed, 15 insertions, 23 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index b8db3dc5ce..cc772e96f3 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 -| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] +| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] => { let hard = List.exists (function | _,((_,(Some { CAst.v = CMeasureRec _ } | Some { CAst.v = CWfRec _}),_,_,_),_) -> true @@ -190,9 +190,7 @@ VERNAC COMMAND EXTEND Function | Vernacextend.VtSideff ids, _ when hard -> Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } - -> { fun ~pstate:ontop -> - let pstate = do_generate_principle false (List.map snd recsl) in - Proof_global.maybe_push ~ontop pstate} + -> { do_generate_principle false (List.map snd recsl) } END { @@ -227,33 +225,32 @@ let warning_error names e = } VERNAC COMMAND EXTEND NewFunctionalScheme -| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] +| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - { fun ~pstate:ontop -> - begin + { begin try - Functional_principles_types.build_scheme fas; ontop + Functional_principles_types.build_scheme fas; None with | Functional_principles_types.No_graph_found -> begin match fas with | (_,fun_name,_)::_ -> begin - let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in - try Functional_principles_types.build_scheme fas; ontop + let pstate = make_graph (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; ontop + 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; ontop + warning_error names e; None end } END @@ -267,6 +264,6 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -| ![ proof ] ["Generate" "graph" "for" reference(c)] -> - { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) } +| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] -> + { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d47c12a7cb..6ea2eb579f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -839,7 +839,9 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph env sigma (f_ref : GlobRef.t) = +let make_graph (f_ref : GlobRef.t) = + let env = Global.env() in + let sigma = Evd.from_env env in let c,c_body = match f_ref with | ConstRef c -> @@ -907,11 +909,4 @@ let make_graph env sigma (f_ref : GlobRef.t) = expr_list; pstate) -let make_graph ~ontop f_ref = - let pstate = Option.map Proof_global.get_current_pstate ontop in - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop - (make_graph env sigma f_ref) - let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index cf4ef23d1a..c803484617 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -17,4 +17,4 @@ val functional_induction : Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option +val make_graph : GlobRef.t -> Proof_global.pstate option |