diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 12 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 3 |
2 files changed, 10 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0fe6913587..100bf347f8 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 diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 883a64b9a1..a5a87b9bdb 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -72,6 +72,9 @@ val non_instantiated : evar_map -> (evar * evar_info) list (***********************************************************) (* Unification utils *) +exception NoHeadEvar +val head_evar : constr -> existential_key (* may raise NoHeadEvar *) + val is_ground_term : evar_defs -> constr -> bool val is_ground_env : evar_defs -> env -> bool val solve_refl : |