diff options
Diffstat (limited to 'pretyping/program.ml')
| -rw-r--r-- | pretyping/program.ml | 55 |
1 files changed, 20 insertions, 35 deletions
diff --git a/pretyping/program.ml b/pretyping/program.ml index 62aedcfb..52d940d8 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -1,34 +1,20 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp open CErrors open Util -open Names -open Term -let make_dir l = DirPath.make (List.rev_map Id.of_string l) - -let find_reference locstr dir s = - 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 -> - 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) - -let init_constant dir s () = coq_constant "Program" dir s -let init_reference dir s () = coq_reference "Program" dir s +let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = + let open EConstr in let gr = delayed_force r in mkApp (Evarutil.e_new_global evdref gr, args) @@ -54,20 +40,22 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" -let coq_not = init_constant ["Init";"Logic"] "not" -let coq_and = init_constant ["Init";"Logic"] "and" +let coq_not = init_reference ["Init";"Logic"] "not" +let coq_and = init_reference ["Init";"Logic"] "and" -let mk_coq_not x = mkApp (delayed_force coq_not, [| x |]) +let mk_coq_not sigma x = + let sigma, notc = Evarutil.new_global sigma (coq_not ()) in + sigma, EConstr.mkApp (notc, [| x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> invalid_arg "unsafe_fold_right" -let mk_coq_and l = - let and_typ = delayed_force coq_and in - unsafe_fold_right +let mk_coq_and sigma l = + let sigma, and_typ = Evarutil.new_global sigma (coq_and ()) in + sigma, unsafe_fold_right (fun c conj -> - mkApp (and_typ, [| c ; conj |])) + EConstr.mkApp (and_typ, [| c ; conj |])) l (* true = transparent by default, false = opaque if possible *) @@ -85,8 +73,7 @@ open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "preferred transparency of Program obligations"; optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; @@ -94,8 +81,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "program cases"; optkey = ["Program";"Cases"]; optread = (fun () -> !program_cases); @@ -103,8 +89,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "program generalized coercion"; optkey = ["Program";"Generalized";"Coercion"]; optread = (fun () -> !program_generalized_coercion); |