From 133ce76b38344b062699cc418e59d400becf27b4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 28 May 2008 19:09:32 +0000
Subject: Notation concise pour la valeur par défaut des cas reconnus comme
 impossibles dans un filtrage dépendant.

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

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ca3347dbbf..73614797a7 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -109,6 +109,14 @@ let arith_module = make_dir ["Coq";"Arith";"Arith"]
 
 (* TODO: temporary hack *)
 let make_kn dir id = Libnames.encode_kn dir id
+let make_con dir id = Libnames.encode_con dir id
+
+(** Identity *)
+
+let id = make_con datatypes_module (id_of_string "id")
+let type_of_id = make_con datatypes_module (id_of_string "ID")
+
+let _ = Cases.set_impossible_default_clause (mkConst id,mkConst type_of_id)
 
 (** Natural numbers *)
 let nat_kn = make_kn datatypes_module (id_of_string "nat")
-- 
cgit v1.2.3