diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof.mli | 2 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 |
5 files changed, 5 insertions, 5 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 8e7c07135f..45ec59ef05 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -20,6 +20,6 @@ val w_refine : evar * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map val instantiate_pf_com : - Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map + Evd.evar -> Constrexpr.constr_expr -> Evd.evar_map -> Evd.evar_map (** the instantiate tactic was moved to [tactics/evar_tactics.ml] *) diff --git a/proofs/goal.mli b/proofs/goal.mli index d67a6b12f3..acda9031b9 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -55,7 +55,7 @@ val return : 'a -> 'a sensitive (* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. In an ideal world, this could/should be the other way round. As of now, though, it seems at least quite useful to build tactics. *) -val interp_constr : Topconstr.constr_expr -> Term.constr sensitive +val interp_constr : Constrexpr.constr_expr -> Term.constr sensitive (* Type of constr with holes used by refine. *) type refinable diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index a271fb3367..9b92893a7d 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -162,7 +162,7 @@ val by : tactic -> unit UserError if no proof is focused or if there is no such [n]th existential variable *) -val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit +val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit (** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) diff --git a/proofs/proof.mli b/proofs/proof.mli index 715b3341b6..e162a2aa0d 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -187,5 +187,5 @@ module V82 : sig val grab_evars : proof -> unit (* Implements the Existential command *) - val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit + val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> unit end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index fe24b54b36..1ae5c4fd2d 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -210,7 +210,7 @@ module V82 : sig val top_evars : proofview -> Evd.evar list (* Implements the Existential command *) - val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview + val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview (* spiwack: [purify] might be useful while writing tactics manipulating exception explicitely or from the [V82] submodule (neither being advised, though *) |