From 90a916ee7e0c995dd6a402b685656a02de3947d6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 4 Jul 2001 15:12:59 +0000
Subject: ajout Show Intro(s)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1825 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics')

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6f315f358b..e57eb11b65 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -59,6 +59,7 @@ val dyn_mutual_cofix : tactic_arg list -> tactic
 (*s Introduction tactics. *)
 
 val next_global_ident_away : identifier -> identifier list -> identifier
+val fresh_id : identifier list -> identifier -> goal sigma -> identifier
 
 val intro                : tactic
 val introf               : tactic
-- 
cgit v1.2.3