diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-08 17:36:28 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-08 17:36:28 +0000 |
commit | 509680e0644a8787d11612948f8b1b36e2de9f18 (patch) | |
tree | 6b7ac08810f23bf89e3fa818b7962780cba440fc /contrib/funind | |
parent | fbb6f2faab29ca3b851b2c710a76b785a8430a89 (diff) |
More exception handling in functional scheme.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7643 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind')
-rw-r--r-- | contrib/funind/tacinv.ml4 | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index d06d39664..517e92d93 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -790,6 +790,7 @@ let buildFunscheme fonc mutflist = (* Here we call the function invfun_proof, that effectively builds the scheme *) (* let princ_proof,levar,_,evararr,absc,parms = *) + let _ = prstr "Recherche du principe... lancement de invfun_proof\n" in let pr = invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in (* parameters are still there (unboud rel), and patternify must not take them -> lift*) @@ -825,10 +826,15 @@ let buildFunscheme fonc mutflist = (* Declaration of the functional scheme. *) let declareFunScheme f fname mutflist = - let id_to_cstr = constr_of_id (Global.env()) in (* careful: env() is evaluated now *) + let _ = prstr "Recherche du perincipe...\n" in + let id_to_cstr id = + try constr_of_id (Global.env()) id + with + Not_found -> error (string_of_id id ^ " not found in the environment") in let flist = if mutflist=[] then [f] else mutflist in let fcstrlist = Array.of_list (List.map id_to_cstr flist) in - let scheme = buildFunscheme (id_to_cstr f) fcstrlist in + let idf = id_to_cstr f in + let scheme = buildFunscheme idf fcstrlist in let _ = prstr "Principe:" in let _ = prconstr scheme in let ce = { |