diff options
| author | jforest | 2006-04-10 15:51:57 +0000 |
|---|---|---|
| committer | jforest | 2006-04-10 15:51:57 +0000 |
| commit | fbf8b216764d8854ceabfe007c26c9b079fd5928 (patch) | |
| tree | ef704fc0cbe666f00506ceec5d66a127dd6ab3ba /contrib/recdef | |
| parent | 264af456f928ee4e329b07449fec6846f78e0d93 (diff) | |
+ Changing a little functional schemes types
+ New tactic to prove functions schemes
+ Add a command "Generate graph for <functionname>" to generate automatiquelly
the graph associated to a function (usefull only when the function
has not been defined by GenFixpoint).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8694 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/recdef')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 36ebaff11f..cf09e63a75 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -53,7 +53,9 @@ let do_observe_tac s tac g = let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in try let v = tac g in msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); v with e -> - msgnl (str "observation "++str s++str " raised exception " ++ Cerrors.explain_exn e ++ str "on goal " ++ goal ); raise e;; + msgnl (str "observation "++str s++str " raised exception " ++ + Cerrors.explain_exn e ++ str "on goal " ++ goal ); + raise e;; let observe_tac s tac g = tac g |