diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-25 14:31:15 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:42:01 +0200 |
| commit | 87910d7be9bd50de4db80f70c6e287c7c7994460 (patch) | |
| tree | ff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /plugins/funind/recdef.ml | |
| parent | 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff) | |
Fix 4.04 warnings
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1e405d2c9..bd30f1159 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1225,6 +1225,7 @@ let get_current_subgoals_types () = let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in sigma, List.map (Goal.V82.abstract_type sigma) sgs +exception EmptySubgoals let build_and_l sigma l = let and_constr = Coqlib.build_coq_and () in let conj_constr = coq_conj () in @@ -1246,7 +1247,7 @@ let build_and_l sigma l = in let l = List.sort compare l in let rec f = function - | [] -> failwith "empty list of subgoals!" + | [] -> raise EmptySubgoals | [p] -> p,tclIDTAC,1 | p1::pl -> let c,tac,nb = f pl in @@ -1432,7 +1433,7 @@ let com_terminate using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type); - with Failure "empty list of subgoals!" -> + with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; defined () |