From 8a905458039b631165d068bbf62f88e11eb36eb1 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Sat, 2 Mar 2013 14:00:46 -0500
Subject: Adapt Y. Bertot's path on private inductives (now the keyword is
 "Private").

A quick and dirty approach to private inductive types
Types for which computable functions are provided, but pattern-matching is disallowed.
This kind of type can be used to simulate simple forms of higher inductive types, with
convertibility for applications of the inductive principle to 0-constructors

Conflicts:
	intf/vernacexpr.mli
	kernel/declarations.ml
	kernel/declarations.mli
	kernel/entries.mli
	kernel/indtypes.ml
	library/declare.ml
	parsing/g_vernac.ml4
	plugins/funind/glob_term_to_relation.ml
	pretyping/indrec.ml
	pretyping/tacred.mli
	printing/ppvernac.ml
	toplevel/vernacentries.ml

Conflicts:
	kernel/declarations.mli
	kernel/declareops.ml
	kernel/indtypes.ml
	kernel/modops.ml
---
 tactics/equality.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 57931f6006..eb8d27f253 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -755,7 +755,8 @@ let descend_then sigma env head dirn =
     try find_rectype env sigma (get_type_of env sigma head)
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
-  let (ind,_),_ = dest_ind_family indf in
+  let indp,_ = (dest_ind_family indf) in
+  let ind, _ = check_privacy env indp in
   let (mib,mip) = lookup_mind_specif env ind in
   let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
@@ -804,7 +805,8 @@ let construct_discriminator sigma env dirn c sort =
       errorlabstrm "Equality.construct_discriminator"
 	(str "Cannot discriminate on inductive constructors with \
 		 dependent types.") in
-  let ((ind,_),_) = dest_ind_family indf in
+  let (indp,_) = dest_ind_family indf in
+  let ind, _ = check_privacy env indp in
   let (mib,mip) = lookup_mind_specif env ind in
   let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
   let deparsign = make_arity_signature env true indf in
-- 
cgit v1.2.3