diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0fe691358..100bf347f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1000,13 +1000,15 @@ let is_ground_env evd env = structures *) let is_ground_env = memo1_2 is_ground_env +exception NoHeadEvar + let head_evar = let rec hrec c = match kind_of_term c with | Evar (evk,_) -> evk | Case (_,_,c,_) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c - | _ -> failwith "headconstant" + | _ -> raise NoHeadEvar in hrec @@ -1107,10 +1109,10 @@ let solve_pattern_eqn env l1 c = *) let status_changed lev (pbty,_,t1,t2) = - try - ExistentialSet.mem (head_evar t1) lev or ExistentialSet.mem (head_evar t2) lev - with Failure _ -> - try ExistentialSet.mem (head_evar t2) lev with Failure _ -> false + try ExistentialSet.mem (head_evar t1) lev + with NoHeadEvar -> + try ExistentialSet.mem (head_evar t2) lev + with NoHeadEvar -> false (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint * definitions. We try to unify the xi with the yi pairwise. The pairs |