From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 pretyping/program.ml | 48 +++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 45 insertions(+), 3 deletions(-)

(limited to 'pretyping/program.ml')

diff --git a/pretyping/program.ml b/pretyping/program.ml
index 0bd121f6..62aedcfb 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -15,10 +15,12 @@ open Term
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
 let find_reference locstr dir s =
-  let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
+  let dp = make_dir dir in
+  let sp = Libnames.make_path dp (Id.of_string s) in
   try Nametab.global_of_path sp
   with Not_found ->
-    anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp)
+    user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++
+      str " has to be required first.")
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
 let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
@@ -67,3 +69,43 @@ let mk_coq_and l =
       (fun c conj ->
 	 mkApp (and_typ, [| c ; conj |]))
       l
+
+(* true = transparent by default, false = opaque if possible *)
+let proofs_transparency = ref true
+let program_cases = ref true
+let program_generalized_coercion = ref true
+
+let set_proofs_transparency = (:=) proofs_transparency
+let get_proofs_transparency () = !proofs_transparency
+
+let is_program_generalized_coercion () = !program_generalized_coercion
+let is_program_cases () = !program_cases
+
+open Goptions
+
+let _ =
+  declare_bool_option
+  { optsync  = true;
+    optdepr  = false;
+    optname  = "preferred transparency of Program obligations";
+    optkey   = ["Transparent";"Obligations"];
+    optread  = get_proofs_transparency;
+    optwrite = set_proofs_transparency; }
+
+let _ =
+  declare_bool_option
+  { optsync  = true;
+    optdepr  = false;
+    optname  = "program cases";
+    optkey   = ["Program";"Cases"];
+    optread  = (fun () -> !program_cases);
+    optwrite = (:=) program_cases }
+
+let _ =
+  declare_bool_option
+  { optsync  = true;
+    optdepr  = false;
+    optname  = "program generalized coercion";
+    optkey   = ["Program";"Generalized";"Coercion"];
+    optread  = (fun () -> !program_generalized_coercion);
+    optwrite = (:=) program_generalized_coercion }
-- 
cgit v1.2.3