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
---
 intf/decl_kinds.mli | 2 ++
 intf/vernacexpr.mli | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 2ed776c2d6..ff77d718bc 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -14,6 +14,8 @@ type binding_kind = Explicit | Implicit
 
 type polymorphic = bool
 
+type private_flag = bool 
+
 type theorem_kind =
   | Theorem
   | Lemma
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ed6ded8e19..0b2e55941a 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -296,7 +296,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * simple_binder with_coercion list
-  | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of private_flag * inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-- 
cgit v1.2.3