summaryrefslogtreecommitdiff
path: root/contrib/funind/indfun_main.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/funind/indfun_main.ml4
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
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)")