diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/funind/functional_principles_types.ml | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/funind/functional_principles_types.ml')
-rw-r--r-- | contrib/funind/functional_principles_types.ml | 32 |
1 files changed, 25 insertions, 7 deletions
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 16076479..b03bdf31 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -552,13 +552,31 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent | _ -> anomaly "" in let (_,(const,_,_)) = - build_functional_principle false - first_type - (Array.of_list sorts) - this_block_funs - 0 - (prove_princ_for_struct false 0 (Array.of_list funs)) - (fun _ _ _ -> ()) + try + build_functional_principle false + first_type + (Array.of_list sorts) + this_block_funs + 0 + (prove_princ_for_struct false 0 (Array.of_list funs)) + (fun _ _ _ -> ()) + with e -> + begin + begin + try + let id = Pfedit.get_current_proof_name () in + let s = string_of_id id in + let n = String.length "___________princ_________" in + if String.length s >= n + then if String.sub s 0 n = "___________princ_________" + then Pfedit.delete_current_proof () + else () + else () + with _ -> () + end; + raise (Defining_principle e) + end + in incr i; let opacity = |