diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /proofs/evar_refiner.mli | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'proofs/evar_refiner.mli')
| -rw-r--r-- | proofs/evar_refiner.mli | 41 |
1 files changed, 5 insertions, 36 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index d57e1b84..9880f2f0 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -6,52 +6,21 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evar_refiner.mli,v 1.28.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) +(*i $Id: evar_refiner.mli 6616 2005-01-21 17:18:23Z herbelin $ i*) (*i*) open Names open Term -open Sign open Environ open Evd open Refiner -open Proof_type (*i*) -type wc = named_context sigma (* for a better reading of the following *) - (* Refinement of existential variables. *) -val rc_of_pfsigma : proof_tree sigma -> wc -val rc_of_glsigma : goal sigma -> wc - -(* A [w_tactic] is a tactic which modifies the a set of evars of which - a goal depend, either by instantiating one, or by declaring a new - dependent goal *) -type w_tactic = wc -> wc - -val startWalk : goal sigma -> wc * (wc -> tactic) - -val extract_decl : evar -> w_tactic -val restore_decl : evar -> evar_info -> w_tactic -val w_Declare : evar -> types -> w_tactic -val w_Define : evar -> constr -> w_tactic - -val w_Underlying : wc -> evar_map -val w_env : wc -> env -val w_hyps : wc -> named_context -val w_whd : wc -> constr -> constr -val w_type_of : wc -> constr -> constr -val w_add_sign : (identifier * types) -> w_tactic +val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs -val w_whd_betadeltaiota : wc -> constr -> constr -val w_hnf_constr : wc -> constr -> constr -val w_conv_x : wc -> constr -> constr -> bool -val w_const_value : wc -> constant -> constr -val w_defined_evar : wc -> existential_key -> bool +val instantiate_pf_com : + int -> Topconstr.constr_expr -> pftreestate -> pftreestate -val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic -(*i -val instantiate_tac : tactic_arg list -> tactic -i*) -val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate +(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) |