1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: evar_refiner.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
20
(******************************************)
21
(* Instantiation of existential variables *)
22
(******************************************)
24
(* w_tactic pour instantiate *)
26
let w_refine evk (ltac_vars,rawc) evd =
27
if Evd.is_defined (evars_of evd) evk then
28
error "Instantiate called on already-defined evar";
29
let e_info = Evd.find (evars_of evd) evk in
30
let env = Evd.evar_env e_info in
32
try Pretyping.Default.understand_ltac
33
(evars_of evd) env ltac_vars (OfType (Some e_info.evar_concl)) rawc
35
let loc = Rawterm.loc_of_rawconstr rawc in
37
(loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
38
string_of_existential evk))
40
evar_define evk typed_c (evars_reset_evd (evars_of evd') evd)
42
(* vernac command Existential *)
44
let instantiate_pf_com n com pfts =
45
let gls = top_goal_of_pftreestate pfts in
46
let sigma = gls.sigma in
48
let evl = Evarutil.non_instantiated sigma in
50
error "incorrect existential variable index"
51
else if List.length evl < n then
52
error "not so many uninstantiated existential variables"
56
let env = Evd.evar_env evi in
57
let rawc = Constrintern.intern_constr sigma env com in
58
let evd = create_goal_evar_defs sigma in
59
let evd' = w_refine evk (([],[]),rawc) evd in
60
change_constraints_pftreestate (evars_of evd') pfts