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

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