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

2 files changed, 10 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
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 883a64b9a..a5a87b9bd 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 :