summaryrefslogtreecommitdiff
path: root/proofs/evar_refiner.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /proofs/evar_refiner.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r--proofs/evar_refiner.ml53
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