diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /proofs/evar_refiner.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r-- | proofs/evar_refiner.ml | 26 |
1 files changed, 7 insertions, 19 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 69168dbd..36268de1 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -1,20 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Names open Term open Evd open Evarutil open Sign -open Proof_trees open Refiner (******************************************) @@ -33,7 +30,7 @@ let define_and_solve_constraints evk c evd = 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) + if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true) pbs) with e when Pretype_errors.precatchable_exception e -> error "Instance does not satisfy constraints." @@ -46,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = 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 + let loc = Glob_term.loc_of_glob_constr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) @@ -55,19 +52,10 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = (* vernac command Existential *) -let instantiate_pf_com n com pfts = - let gls = top_goal_of_pftreestate pfts in - let sigma = gls.sigma in - let (evk,evi) = - let evl = Evarutil.non_instantiated sigma in - if (n <= 0) then - error "incorrect existential variable index" - else if List.length evl < n then - error "not so many uninstantiated existential variables" - else - List.nth evl (n-1) - in +(* Main component of vernac command Existential *) +let instantiate_pf_com evk com sigma = + let evi = Evd.find sigma evk in let env = Evd.evar_env evi in let rawc = Constrintern.intern_constr sigma env com in let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in - change_constraints_pftreestate sigma' pfts + sigma' |