diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 17:47:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 17:57:20 +0200 |
| commit | 0e2189a7a070dd356d5e549392d35d9d07b05058 (patch) | |
| tree | 010ef6230603cb3beb91e9058fe0e1adb733c5d6 /toplevel | |
| parent | b857552b6ffd5e72b5124aee9e35fc5c14607173 (diff) | |
Factorizing the uses of Declareops.safe_flags.
This allows a smooth addition of various unsafe flags without wreaking
havoc in the ML codebase.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 10 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 6f2dd1bf1..ff43cd495 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -179,7 +179,7 @@ let declare_definition ~flags ident (local, p, k) ce pl imps hook = Lemmas.call_hook fix_exn hook local r let _ = Obligations.declare_definition_ref := - (fun i k c imps hook -> declare_definition ~flags:{Declarations.check_guarded=true} i k c [] imps hook) + (fun i k c imps hook -> declare_definition ~flags:Declareops.safe_flags i k c [] imps hook) let do_definition ident k pl bl red_option c ctypopt hook = let (ce, evd, pl', imps as def) = @@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce pl' imps + ignore(declare_definition ~flags:Declareops.safe_flags ident k ce pl' imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -838,7 +838,7 @@ let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),ef declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := - (fun ?opaque k ctx f d t imps -> declare_fix ~flags:{Declarations.check_guarded=true} ?opaque k [] ctx f d t imps) + (fun ?opaque k ctx f d t imps -> declare_fix ~flags:Declareops.safe_flags ?opaque k [] ctx f d t imps) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1269,11 +1269,11 @@ let do_program_recursive local p fixkind fixl ntns = in let indexes = Pretyping.search_guard - ~tflags:{Declarations.check_guarded=true} + ~tflags:Declareops.safe_flags Loc.ghost (Global.env ()) possible_indexes fixdecls in List.iteri (fun i _ -> Inductive.check_fix env - ~flags:{Declarations.check_guarded=true} + ~flags:Declareops.safe_flags ((indexes,i),fixdecls)) fixl end in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 00fd97210..3d15f2142 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -567,7 +567,7 @@ let declare_mutual_definition l = List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in let indexes = - Pretyping.search_guard ~tflags:{Declarations.check_guarded=true} + Pretyping.search_guard ~tflags:Declareops.safe_flags Loc.ghost (Global.env()) possible_indexes fixdecls in Some indexes, diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0b4dc0d18..5131a4179 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1731,7 +1731,7 @@ let vernac_load interp fname = try while true do interp (snd (parse_sentence input)) done with End_of_input -> () -let all_checks = { Declarations.check_guarded = true } +let all_checks = Declareops.safe_flags (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands |