summaryrefslogtreecommitdiff
path: root/contrib/funind/indfun_main.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind/indfun_main.ml4')
-rw-r--r--contrib/funind/indfun_main.ml45
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 26a1066c..9cee9edc 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -203,7 +203,10 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
match fas with
| (_,fun_name,_)::_ ->
begin
- make_graph (Nametab.global fun_name);
+ begin
+ make_graph (Nametab.global fun_name)
+ end
+ ;
try Functional_principles_types.build_scheme fas
with Functional_principles_types.No_graph_found ->
Util.error ("Cannot generate induction principle(s)")