diff options
| author | herbelin | 2009-10-30 14:10:20 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-30 14:10:20 +0000 |
| commit | 4da1d9ee92f6764e8dee236730652391323a2ec5 (patch) | |
| tree | fba873b3caee9cba6fd2970de4d9d9beedabaa84 /proofs | |
| parent | cb6a920659b8e67092ce21ffe94895d102887c24 (diff) | |
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
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 *) |