diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5beebe690..838bf22c66 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -32,8 +32,6 @@ exception Elimconst let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Generate weak constraints between Irrelevant universes"; optkey = ["Cumulativity";"Weak";"Constraints"]; optread = (fun () -> not !UState.drop_weak_constraints); optwrite = (fun a -> UState.drop_weak_constraints:=not a); @@ -972,8 +970,6 @@ module CredNative = RedNative(CNativeEntries) let debug_RAKAM = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states of the Reductionops abstract machine"; optkey = ["Debug";"RAKAM"]; optread = (fun () -> !debug_RAKAM); optwrite = (fun a -> debug_RAKAM:=a); @@ -1711,7 +1707,7 @@ let splay_arity env sigma c = let l, c = splay_prod env sigma c in match EConstr.kind sigma c with | Sort s -> l,s - | _ -> invalid_arg "splay_arity" + | _ -> raise Reduction.NotArity let sort_of_arity env sigma c = snd (splay_arity env sigma c) |