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

3 files changed, 29 insertions, 6 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 :
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 25c668f5d..b3976704a 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Term
 open Evd
+open Evarutil
 open Sign
 open Proof_trees
 open Refiner
@@ -20,6 +21,23 @@ open Refiner
 (* Instantiation of existential variables *)
 (******************************************)
 
+let depends_on_evar evk _ (pbty,_,t1,t2) =
+  try head_evar t1 = evk
+  with NoHeadEvar ->
+  try head_evar t2 = evk
+  with NoHeadEvar -> false
+
+let define_and_solve_constraints evk c evd =
+  try
+    let evd = define evk c evd in
+    let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
+    fst (List.fold_left
+      (fun (evd,b as p) (pbty,env,t1,t2) ->
+	if b then Evarconv.evar_conv_x env evd pbty t1 t2 else p) (evd,true)
+      pbs)
+  with e when Pretype_errors.precatchable_exception e ->
+    error "Instance does not satisfy constraints."
+
 let w_refine (evk,evi) (ltac_var,rawc) sigma =
   if Evd.is_defined sigma evk then
     error "Instantiate called on already-defined evar";
@@ -33,7 +51,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
-    define evk typed_c (evars_reset_evd sigma' sigma)
+  define_and_solve_constraints evk typed_c (evars_reset_evd sigma' sigma)
 
 (* vernac command Existential *)