diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 25c668f5dd..b3976704af 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 *) |