From 392300a73bc4e57d2be865d9a8d77c608ef02f59 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:50 +0000
Subject: New files intf/constrexpr.mli and intf/notation_term.mli out of
 Topconstr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.mli | 2 +-
 proofs/goal.mli         | 2 +-
 proofs/pfedit.mli       | 2 +-
 proofs/proof.mli        | 2 +-
 proofs/proofview.mli    | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'proofs')

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 *)
-- 
cgit v1.2.3