diff options
| author | jforest | 2008-11-24 12:54:19 +0000 |
|---|---|---|
| committer | jforest | 2008-11-24 12:54:19 +0000 |
| commit | f9e72471a81f3b5c22b3d26d434481adf752d3bf (patch) | |
| tree | 982f0672cdb17f410c3e2172a1ceb793a2c16a1e | |
| parent | 31eac37de7a01bf67be3e5547792794f97142f25 (diff) | |
amelioration mineur du comportement de Function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11625 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index d54aca4e6e..62f1148320 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -863,6 +863,8 @@ let is_res id = String.sub (string_of_id id) 0 3 = "res" with Invalid_argument _ -> false + +exception Continue (* The second phase which reconstruct the real type of the constructor. rebuild the raw constructors expression. @@ -908,7 +910,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin try observe (str "computing new type for eq : " ++ pr_rawconstr rt); - let t' = Pretyping.Default.understand Evd.empty env t in + let t' = + try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue + in let is_in_b = is_free_in id b in let _keep_eq = not (List.exists (is_free_in id) args) || is_in_b || @@ -927,7 +931,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) subst_b in mkRProd(n,t,new_b),id_to_exclude - with _ -> + with Continue -> let jmeq = Libnames.IndRef (destInd (jmeq ())) in let ty' = Pretyping.Default.understand Evd.empty env ty in let ind,args' = Inductive.find_inductive env ty' in |