Take constraints into account in the "instantiate" tactic

(building an example that needs it to do).



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

1 files changed, 7 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