From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Mon, 15 Oct 2007 19:55:12 +0000
Subject: Imported Upstream version 8.1.pl2+dfsg

---
 interp/constrextern.ml | 4 +++-
 interp/coqlib.ml       | 4 +++-
 interp/coqlib.mli      | 3 ++-
 3 files changed, 8 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 349e8629..b9d7694f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: constrextern.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -923,6 +923,8 @@ let rec raw_of_pat env = function
   | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
       RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
+  | PCase (_,PMeta None,tm,[||]) ->
+      RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[])
   | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
       let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
       let brns = Array.to_list cstr_nargs in
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 79a217a1..0c3ffd0c 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqlib.ml 8866 2006-05-28 16:21:04Z herbelin $ *)
+(* $Id: coqlib.ml 10067 2007-08-09 17:13:16Z msozeau $ *)
 
 open Util
 open Pp
@@ -236,6 +236,7 @@ let coq_I      = lazy_init_constant ["Logic"] "I"
 (* Connectives *)
 let coq_not = lazy_init_constant ["Logic"] "not"
 let coq_and = lazy_init_constant ["Logic"] "and"
+let coq_conj = lazy_init_constant ["Logic"] "conj"
 let coq_or = lazy_init_constant ["Logic"] "or"
 let coq_ex = lazy_init_constant ["Logic"] "ex"
 
@@ -246,6 +247,7 @@ let build_coq_I ()     = Lazy.force coq_I
 let build_coq_False () = Lazy.force coq_False
 let build_coq_not ()   = Lazy.force coq_not
 let build_coq_and ()   = Lazy.force coq_and
+let build_coq_conj ()  = Lazy.force coq_conj
 let build_coq_or ()   = Lazy.force coq_or
 let build_coq_ex ()   = Lazy.force coq_ex
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index c81d72de..7254800c 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqlib.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: coqlib.mli 10067 2007-08-09 17:13:16Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -129,6 +129,7 @@ val build_coq_not : constr delayed
 
 (* Conjunction *)
 val build_coq_and : constr delayed
+val build_coq_conj : constr delayed
 
 (* Disjunction *)
 val build_coq_or : constr delayed
-- 
cgit v1.2.3