diff options
| author | jforest | 2006-06-06 16:07:41 +0000 |
|---|---|---|
| committer | jforest | 2006-06-06 16:07:41 +0000 |
| commit | eed31762296482499ae843e030249b50761e4a5e (patch) | |
| tree | 8a2a30137cebc6835cd59e581dee79fec2b6365f | |
| parent | 1219a88094303f560cef6df95f75633bde8fd5e8 (diff) | |
Error in last commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8903 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 3f3f87966d..00009d74ee 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -446,12 +446,17 @@ let make_scheme fas = let env = Global.env () and sigma = Evd.empty in let id_to_constr id = - try Tacinterp.constr_of_id env id - with Not_found -> - Util.error ("Cannot find "^ string_of_id id) in - let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in + let funs = + List.map + (fun (_,f,_) -> + try id_to_constr f + with Not_found -> + Util.error ("Cannot find "^ string_of_id id) + ) + fas + in let first_fun = destConst (List.hd funs) in let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in |
