Pas très propre de reposer sur la capture des anomalies (et cela

complique le débogage...). Réécriture de 2 morceaux de code qui
utilisaient les anomalies à des fins détournées de leur intention.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10653 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 11 insertions, 4 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c583a0b22..e044c17a9 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -512,11 +512,16 @@ let metas_of evd =
     | (n,Cltyp (_,typ))  -> (n,typ.rebus))
     (meta_list evd)
 
+let meta_opt_fvalue evd mv =
+  match Metamap.find mv evd.metas with
+    | Clval(_,b,_) -> Some b
+    | Cltyp _ -> None
+
 let meta_defined evd mv =
   match Metamap.find mv evd.metas with
     | Clval _ -> true
     | Cltyp _ -> false
- 
+
 let meta_fvalue evd mv =
   match Metamap.find mv evd.metas with
     | Clval(_,b,_) -> b
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index d74d21446..7f5a4060b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -183,6 +183,7 @@ val meta_defined : evar_defs -> metavariable -> bool
 (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
    meta has no value *)  
 val meta_fvalue    : evar_defs -> metavariable -> constr freelisted * instance_status
+val meta_opt_fvalue : evar_defs -> metavariable -> (constr freelisted * instance_status) option
 val meta_ftype     : evar_defs -> metavariable -> constr freelisted
 val meta_name      : evar_defs -> metavariable -> name
 val meta_with_name : evar_defs -> identifier -> metavariable
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 617bd7717..c7af265ce 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -929,8 +929,9 @@ let meta_value evd mv =
 let meta_reducible_instance evd b =
   let fm = Metaset.elements b.freemetas in
   let metas = List.fold_left (fun l mv -> 
-    try let g,(_,s) = meta_fvalue evd mv in (mv,(g.rebus,s))::l 
-    with Anomaly _ | Not_found -> l) [] fm in 
+    match (try meta_opt_fvalue evd mv with Not_found -> None) with
+    | Some (g,(_,s)) -> (mv,(g.rebus,s))::l 
+    | None -> l) [] in
   let rec irec u =
     let u = whd_betaiota u in
     match kind_of_term u with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5f919a4db..c3e79c6f0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1947,7 +1947,7 @@ let compute_elim_sig ?elimc elimt =
     elimc = elimc; elimt = elimt; concl = conclusion;
     predicates = preds; npredicates = List.length preds; 
     branches = branches; nbranches = List.length branches; 
-    farg_in_concl = (try isApp (last_arg ccl) with _ -> false);
+    farg_in_concl = isApp ccl && isApp (last_arg ccl);
     params = params; nparams = nparams; 
     (* all other fields are unsure at this point. Including these:*)
     args = args_indargs; nargs = List.length args_indargs; } in