diff options
Diffstat (limited to 'proofs/evar_refiner.ml')
| -rw-r--r-- | proofs/evar_refiner.ml | 53 |
1 files changed, 33 insertions, 20 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index f4613f8d..e4fab3f2 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,45 +6,59 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml 12102 2009-04-24 10:48:11Z herbelin $ *) +(* $Id$ *) open Util open Names open Term open Evd +open Evarutil open Sign open Proof_trees open Refiner -open Pretyping (******************************************) (* Instantiation of existential variables *) (******************************************) -(* w_tactic pour instantiate *) +let depends_on_evar evk _ (pbty,_,t1,t2) = + try head_evar t1 = evk + with NoHeadEvar -> + try head_evar t2 = evk + with NoHeadEvar -> false -let w_refine evk (ltac_vars,rawc) evd = - if Evd.is_defined (evars_of evd) evk then +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"; - let e_info = Evd.find (evars_of evd) evk in - let env = Evd.evar_env e_info in - let evd',typed_c = - try Pretyping.Default.understand_ltac - (evars_of evd) env ltac_vars (OfType (Some e_info.evar_concl)) rawc + let env = Evd.evar_env evi in + let sigma',typed_c = + try Pretyping.Default.understand_ltac true sigma env ltac_var + (Pretyping.OfType (Some evi.evar_concl)) rawc with _ -> let loc = Rawterm.loc_of_rawconstr rawc in - user_err_loc + user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) in - evar_define evk typed_c (evars_reset_evd (evars_of evd') evd) + define_and_solve_constraints evk typed_c (evars_reset_evd sigma' sigma) (* vernac command Existential *) -let instantiate_pf_com n com pfts = +let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in - let sigma = gls.sigma in - let (evk,evi) = + let sigma = gls.sigma in + let (evk,evi) = let evl = Evarutil.non_instantiated sigma in if (n <= 0) then error "incorrect existential variable index" @@ -52,9 +66,8 @@ let instantiate_pf_com n com pfts = error "not so many uninstantiated existential variables" else List.nth evl (n-1) - in + in let env = Evd.evar_env evi in - let rawc = Constrintern.intern_constr sigma env com in - let evd = create_goal_evar_defs sigma in - let evd' = w_refine evk (([],[]),rawc) evd in - change_constraints_pftreestate (evars_of evd') pfts + let rawc = Constrintern.intern_constr sigma env com in + let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in + change_constraints_pftreestate sigma' pfts |