aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorjforest2006-06-06 16:07:41 +0000
committerjforest2006-06-06 16:07:41 +0000
commiteed31762296482499ae843e030249b50761e4a5e (patch)
tree8a2a30137cebc6835cd59e581dee79fec2b6365f
parent1219a88094303f560cef6df95f75633bde8fd5e8 (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.ml13
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