aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/evd.ml7
-rw-r--r--pretyping/evd.mli1
-rw-r--r--pretyping/reductionops.ml5
-rw-r--r--tactics/tactics.ml2
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