From 5303c048a763d0f9d0b2fd2c14647a78f8157360 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 22 Jun 2006 22:01:44 +0000
Subject: Nettoyage, uniformisation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8971 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.mli | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

(limited to 'tactics/tacinterp.mli')

diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c799d47e4..057f20be5 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -11,6 +11,7 @@
 (*i*)
 open Dyn
 open Pp
+open Util
 open Names
 open Proof_type
 open Tacmach
@@ -20,6 +21,7 @@ open Tacexpr
 open Genarg
 open Topconstr
 open Mod_subst
+open Redexpr
 (*i*)
 
 (* Values for interpretation *)
@@ -39,12 +41,6 @@ and interp_sign =
   { lfun : (identifier * value) list;
     debug : debug_info }
 
-(* Gives the identifier corresponding to an Identifier [tactic_arg] *)
-val id_of_Identifier : Environ.env -> value -> identifier
-
-(* Gives the constr corresponding to a Constr [value] *)
-val constr_of_VConstr : Environ.env -> value -> constr
-
 (* Transforms an id into a constr if possible *)
 val constr_of_id : Environ.env -> identifier -> constr
 
@@ -103,16 +99,18 @@ val subst_rawconstr_and_expr :
 (* Interprets any expression *)
 val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
 
+(* Interprets an expression that evaluates to a constr *)
+val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> 
+  constr
+
 (* Interprets redexp arguments *)
-val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr
-  -> Redexpr.red_expr
+val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr
 
 (* Interprets tactic expressions *)
 val interp_tac_gen : (identifier * value) list -> 
                  debug_info -> raw_tactic_expr -> tactic
 
-val interp_hyp :  interp_sign -> goal sigma -> 
-  identifier Util.located -> identifier
+val interp_hyp :  interp_sign -> goal sigma -> identifier located -> identifier
 
 (* Initial call for interpretation *)
 val glob_tactic : raw_tactic_expr -> glob_tactic_expr
-- 
cgit v1.2.3