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
---
 plugins/funind/glob_term_to_relation.ml | 6 +++---
 plugins/funind/merge.ml                 | 3 ++-
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4544f736ca..41970fce83 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1405,7 +1405,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) true
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
@@ -1416,7 +1416,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1431,7 +1431,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,false,repacked_rel_inds))
 	    ++ fnl () ++
 	    Errors.print reraise
 	in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 2e524a35f0..6eabe6e871 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -884,7 +884,8 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in
+  let mie,impls = Command.interp_mutual_inductive indl [] 
+          false (*FIXMEnon-poly *) false (* means not private *) true (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
 
-- 
cgit v1.2.3