aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml14
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/detyping.ml16
-rw-r--r--pretyping/evarconv.ml14
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/program.ml6
-rw-r--r--pretyping/reductionops.ml28
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/unification.ml28
10 files changed, 57 insertions, 59 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 5061aeff88..7104b8586e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -184,13 +184,13 @@ let cofixp_reducible flgs _ stk =
false
let debug_cbv = ref false
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname = "cbv visited constants display";
- Goptions.optkey = ["Debug";"Cbv"];
- Goptions.optread = (fun () -> !debug_cbv);
- Goptions.optwrite = (fun a -> debug_cbv:=a);
-}
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname = "cbv visited constants display";
+ optkey = ["Debug";"Cbv"];
+ optread = (fun () -> !debug_cbv);
+ optwrite = (fun a -> debug_cbv:=a);
+})
let debug_pr_key = function
| ConstKey (sp,_) -> Names.Constant.print sp
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 2c2a8fe49e..1edcc499f0 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -401,7 +401,7 @@ let add_class cl =
let automatically_import_coercions = ref false
open Goptions
-let _ =
+let () =
declare_bool_option
{ optdepr = true; (* remove in 8.8 *)
optname = "automatic import of coercions";
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e21c2fda85..30eb70d0e7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -35,7 +35,7 @@ open Globnames
let use_typeclasses_for_conversion = ref true
-let _ =
+let () =
Goptions.(declare_bool_option
{ optdepr = false;
optname = "use typeclass resolution during conversion";
@@ -183,7 +183,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
with UnableToUnify _ ->
let (n, eqT), restT = dest_prod typ in
let (n', eqT'), restT' = dest_prod typ' in
- let _ =
+ let () =
try evdref := the_conv_x_leq env eqT eqT' !evdref
with UnableToUnify _ -> raise NoSubtacCoercion
in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 072ac9deed..33ced6d6e0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -138,7 +138,7 @@ open Goptions
let wildcard_value = ref true
let force_wildcard () = !wildcard_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "forced wildcard";
optkey = ["Printing";"Wildcard"];
@@ -148,7 +148,7 @@ let _ = declare_bool_option
let synth_type_value = ref true
let synthetize_type () = !synth_type_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "pattern matching return type synthesizability";
optkey = ["Printing";"Synth"];
@@ -158,7 +158,7 @@ let _ = declare_bool_option
let reverse_matching_value = ref true
let reverse_matching () = !reverse_matching_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "pattern-matching reversibility";
optkey = ["Printing";"Matching"];
@@ -168,7 +168,7 @@ let _ = declare_bool_option
let print_primproj_params_value = ref false
let print_primproj_params () = !print_primproj_params_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "printing of primitive projection parameters";
optkey = ["Printing";"Primitive";"Projection";"Parameters"];
@@ -178,7 +178,7 @@ let _ = declare_bool_option
let print_primproj_compatibility_value = ref false
let print_primproj_compatibility () = !print_primproj_compatibility_value
-let _ = declare_bool_option
+let () = declare_bool_option
{ optdepr = false;
optname = "backwards-compatible printing of primitive projections";
optkey = ["Printing";"Primitive";"Projection";"Compatibility"];
@@ -257,8 +257,7 @@ let lookup_index_as_renamed env sigma t n =
let print_factorize_match_patterns = ref true
-let _ =
- let open Goptions in
+let () =
declare_bool_option
{ optdepr = false;
optname = "factorization of \"match\" patterns in printing";
@@ -268,8 +267,7 @@ let _ =
let print_allow_match_default_clause = ref true
-let _ =
- let open Goptions in
+let () =
declare_bool_option
{ optdepr = false;
optname = "possible use of \"match\" default pattern in printing";
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f370ad7ae2..6c268de3b3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -33,14 +33,14 @@ type unify_fun = TransparentState.t ->
env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
let debug_unification = ref (false)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Print states sent to Evarconv unification";
- Goptions.optkey = ["Debug";"Unification"];
- Goptions.optread = (fun () -> !debug_unification);
- Goptions.optwrite = (fun a -> debug_unification:=a);
-}
+ optkey = ["Debug";"Unification"];
+ optread = (fun () -> !debug_unification);
+ optwrite = (fun a -> debug_unification:=a);
+})
(*******************************************)
(* Functions to deal with impossible cases *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index abf52d2893..3391750209 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -108,7 +108,7 @@ let search_guard ?loc env possible_indexes fixdefs =
let strict_universe_declarations = ref true
let is_strict_universe_declarations () = !strict_universe_declarations
-let _ =
+let () =
Goptions.(declare_bool_option
{ optdepr = false;
optname = "strict universe declaration";
diff --git a/pretyping/program.ml b/pretyping/program.ml
index bbabbefdc3..7e38c09189 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -75,7 +75,7 @@ let is_program_cases () = !program_cases
open Goptions
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "preferred transparency of Program obligations";
@@ -83,7 +83,7 @@ let _ =
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "program cases";
@@ -91,7 +91,7 @@ let _ =
optread = (fun () -> !program_cases);
optwrite = (:=) program_cases }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "program generalized coercion";
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e632976ae5..a57ee6e292 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,14 +29,14 @@ exception Elimconst
their parameters in its stack.
*)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Generate weak constraints between Irrelevant universes";
- Goptions.optkey = ["Cumulativity";"Weak";"Constraints"];
- Goptions.optread = (fun () -> not !UState.drop_weak_constraints);
- Goptions.optwrite = (fun a -> UState.drop_weak_constraints:=not a);
-}
+ optkey = ["Cumulativity";"Weak";"Constraints"];
+ optread = (fun () -> not !UState.drop_weak_constraints);
+ optwrite = (fun a -> UState.drop_weak_constraints:=not a);
+})
(** Support for reduction effects *)
@@ -830,14 +830,14 @@ let fix_recarg ((recindices,bodynum),_) stack =
*)
let debug_RAKAM = ref (false)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Print states of the Reductionops abstract machine";
- Goptions.optkey = ["Debug";"RAKAM"];
- Goptions.optread = (fun () -> !debug_RAKAM);
- Goptions.optwrite = (fun a -> debug_RAKAM:=a);
-}
+ optkey = ["Debug";"RAKAM"];
+ optread = (fun () -> !debug_RAKAM);
+ optwrite = (fun a -> debug_RAKAM:=a);
+})
let equal_stacks sigma (x, l) (y, l') =
let f_equal x y = eq_constr sigma x y in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4aea2c3db9..c68890a87f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -37,7 +37,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
open Goptions
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "check that typeclasses proof search returns unique solutions";
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8c1aae26ae..094fcd923e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,25 +43,25 @@ module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname = "Unification is keyed";
- Goptions.optkey = ["Keyed";"Unification"];
- Goptions.optread = (fun () -> !keyed_unification);
- Goptions.optwrite = (fun a -> keyed_unification:=a);
-}
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname = "Unification is keyed";
+ optkey = ["Keyed";"Unification"];
+ optread = (fun () -> !keyed_unification);
+ optwrite = (fun a -> keyed_unification:=a);
+})
let is_keyed_unification () = !keyed_unification
let debug_unification = ref (false)
-let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
- Goptions.optname =
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
"Print states sent to tactic unification";
- Goptions.optkey = ["Debug";"Tactic";"Unification"];
- Goptions.optread = (fun () -> !debug_unification);
- Goptions.optwrite = (fun a -> debug_unification:=a);
-}
+ optkey = ["Debug";"Tactic";"Unification"];
+ optread = (fun () -> !debug_unification);
+ optwrite = (fun a -> debug_unification:=a);
+})
(** Making this unification algorithm correct w.r.t. the evar-map abstraction
breaks too much stuff. So we redefine incorrect functions here. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 23:38:30 +0000