From 5e06a8ef480a68b20f94814b4b2fee1df3d192fd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2003 21:06:33 +0000
Subject: Amélioration afficheur de Cases pour les constr_pattern Déplacement
 traducteur de nom dans Constrextern pour accès aux noms longs Extension du
 traducteur de nom Ajout notation c.(f) en v8 pour les projections de Record

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

(limited to 'interp/constrextern.mli')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index cb58ca58ee..e5cfd0190f 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -22,6 +22,11 @@ open Topconstr
 open Symbols
 (*i*)
 
+(* v7->v8 translation *)
+val id_of_v7_string : string -> identifier
+val v7_to_v8_id : identifier -> identifier (* v7->v8 translation *)
+val shortest_qualid_of_v7_global : Idset.t -> global_reference -> qualid
+
 (* Translation of pattern, cases pattern, rawterm and term into syntax
    trees for printing *)
 
-- 
cgit v1.2.3