diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /proofs/evar_refiner.ml | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r-- | proofs/evar_refiner.ml | 30 |
1 files changed, 9 insertions, 21 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 69168dbd..f271a6bd 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-2012 *) (* \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." @@ -43,10 +40,10 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = error "Instantiate called on already-defined evar"; let env = Evd.evar_env evi in let sigma',typed_c = - try Pretyping.Default.understand_ltac true sigma env ltac_var + try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc - with _ -> - let loc = Rawterm.loc_of_rawconstr rawc in + with e when Errors.noncritical e -> + 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' |