diff options
Diffstat (limited to 'plugins/funind/g_indfun.mlg')
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 54 |
1 files changed, 26 insertions, 28 deletions
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 |