Funind: use maybe_open_proof a bit less

3 files changed, 10 insertions, 10 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 8c9b1e7ba4..bdd30aae0a 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -224,33 +224,33 @@ let warning_error names e =
 
 }
 
-VERNAC COMMAND EXTEND NewFunctionalScheme STATE maybe_open_proof
+VERNAC COMMAND EXTEND NewFunctionalScheme
 | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
     { begin
         try
-          Functional_principles_types.build_scheme fas; None
+          Functional_principles_types.build_scheme fas
         with
         | Functional_principles_types.No_graph_found ->
           begin
             match fas with
             | (_,fun_name,_)::_ ->
               begin
-                let pstate = make_graph (Smartlocate.global_with_alias fun_name) in
-                try Functional_principles_types.build_scheme fas; pstate
+                make_graph (Smartlocate.global_with_alias fun_name);
+                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; pstate
+                  warning_error names e
               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; None
+          warning_error names e
       end
     }
 END
@@ -263,7 +263,7 @@ VERNAC COMMAND EXTEND NewFunctionalCase
 END
 
 (***** debug only ***)
-VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY STATE maybe_open_proof
+VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 | ["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 6ea2eb579f..16df34e214 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -903,10 +903,10 @@ let make_graph (f_ref : GlobRef.t) =
 	 in
          let mp = Constant.modpath c in
          let pstate = do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list in
+         assert (Option.is_empty pstate);
 	 (* We register the infos *)
 	 List.iter
            (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
-           expr_list;
-         pstate)
+           expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index c803484617..cd39266378 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 : GlobRef.t -> Proof_global.pstate option
+val make_graph : GlobRef.t -> unit