From e7d592ada2d681876d2bcf0a45d4267b3746064f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:41:55 +0000
Subject: Mise en place d'un système optionnel de discharge immédiat; prise en
 compte des défs locales dans les arguments des inductifs; nettoyage divers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index 8b1cb71a13..fc3453611c 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -235,6 +235,10 @@ let next_name_away name l =
     | Name str  -> next_ident_away str l
     | Anonymous -> id_of_string "_"
 
+let out_name = function
+  | Name id -> id
+  | Anonymous -> anomaly "out_name: expects a defined name"
+
 (* Kinds *)
 
 type path_kind = CCI | FW | OBJ
-- 
cgit v1.2.3