aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--dev/ci/user-overlays/06923-ppedrot-export-options.sh7
-rw-r--r--ide/ide_slave.ml6
-rw-r--r--intf/vernacexpr.ml5
-rw-r--r--kernel/cClosure.ml103
-rw-r--r--kernel/cClosure.mli20
-rw-r--r--kernel/reduction.ml136
-rw-r--r--library/goptions.ml57
-rw-r--r--library/goptions.mli15
-rw-r--r--parsing/g_vernac.ml435
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--plugins/ssr/ssrvernac.ml42
-rw-r--r--pretyping/cbv.ml8
-rw-r--r--pretyping/inferCumulativity.ml10
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/typing.ml56
-rw-r--r--printing/ppvernac.ml15
-rw-r--r--stm/vernac_classifier.ml8
-rw-r--r--vernac/vernacentries.ml56
-rw-r--r--vernac/vernacprop.ml2
20 files changed, 284 insertions, 264 deletions
diff --git a/CHANGES b/CHANGES
index 320b325ae5..25a519f159 100644
--- a/CHANGES
+++ b/CHANGES
@@ -81,6 +81,9 @@ Vernacular Commands
- An experimental command "Show Extraction" allows to extract the content
of the current ongoing proof (grant wish #4129).
- Coercion now accepts the type of its argument to be "Prop" or "Type".
+- The "Export" modifier can now be used when setting and unsetting options, and
+ will result in performing the same change when the module corresponding the
+ command is imported.
Universes
diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh
new file mode 100644
index 0000000000..333a9e84bd
--- /dev/null
+++ b/dev/ci/user-overlays/06923-ppedrot-export-options.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then
+ ltac2_CI_BRANCH=export-options
+ ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+ Equations_CI_BRANCH=export-options
+ Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 0ba1b3a4fb..55b4fa87e6 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -57,8 +57,8 @@ let coqide_known_option table = List.mem table [
["Printing";"Unfocused"]]
let is_known_option cmd = match Vernacprop.under_control cmd with
- | VernacSetOption (o,BoolValue true)
- | VernacUnsetOption o -> coqide_known_option o
+ | VernacSetOption (_, o, BoolValue true)
+ | VernacUnsetOption (_, o) -> coqide_known_option o
| _ -> false
(** Check whether a command is forbidden in the IDE *)
@@ -340,7 +340,7 @@ let set_options options =
| IntValue i -> Goptions.set_int_option_value name i
| StringValue s -> Goptions.set_string_option_value name s
| StringOptValue (Some s) -> Goptions.set_string_option_value name s
- | StringOptValue None -> Goptions.unset_option_value_gen None name
+ | StringOptValue None -> Goptions.unset_option_value_gen name
in
List.iter iter options
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 0a6e5b3b31..dca4910574 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -425,9 +425,8 @@ type nonrec vernac_expr =
| VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
| VernacSetStrategy of
(Conv_oracle.level * reference or_by_notation list) list
- | VernacUnsetOption of Goptions.option_name
- | VernacSetOption of Goptions.option_name * option_value
- | VernacSetAppendOption of Goptions.option_name * string
+ | VernacUnsetOption of export_flag * Goptions.option_name
+ | VernacSetOption of export_flag * Goptions.option_name * option_value
| VernacAddOption of Goptions.option_name * option_ref_value list
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_value list
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 11faef02cb..5f683790c1 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -259,12 +259,14 @@ module KeyTable = Hashtbl.Make(IdKeyHash)
let eq_table_key = IdKeyHash.equal
+type 'a infos_tab = 'a KeyTable.t
+
type 'a infos_cache = {
- i_repr : 'a infos -> constr -> 'a;
+ i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
i_env : env;
i_sigma : existential -> constr option;
i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t;
- i_tab : 'a KeyTable.t }
+}
and 'a infos = {
i_flags : reds;
@@ -279,9 +281,9 @@ let assoc_defined id env = match Environ.lookup_named id env with
| LocalDef (_, c, _) -> c
| _ -> raise Not_found
-let ref_value_cache ({i_cache = cache} as infos) ref =
+let ref_value_cache ({i_cache = cache} as infos) tab ref =
try
- Some (KeyTable.find cache.i_tab ref)
+ Some (KeyTable.find tab ref)
with Not_found ->
try
let body =
@@ -300,8 +302,8 @@ let ref_value_cache ({i_cache = cache} as infos) ref =
| VarKey id -> assoc_defined id cache.i_env
| ConstKey cst -> constant_value_in cache.i_env cst
in
- let v = cache.i_repr infos body in
- KeyTable.add cache.i_tab ref v;
+ let v = cache.i_repr infos tab body in
+ KeyTable.add tab ref v;
Some v
with
| Not_found (* List.assoc *)
@@ -318,7 +320,7 @@ let create mk_cl flgs env evars =
i_env = env;
i_sigma = evars;
i_rels = (Environ.pre_env env).env_rel_context.env_rel_map;
- i_tab = KeyTable.create 17 }
+ }
in { i_flags = flgs; i_cache = cache }
@@ -906,23 +908,23 @@ and knht info e t stk =
(************************************************************************)
(* Computes a weak head normal form from the result of knh. *)
-let rec knr info m stk =
+let rec knr info tab m stk =
match m.term with
| FLambda(n,tys,f,e) when red_set info.i_flags fBETA ->
(match get_args n tys f e stk with
- Inl e', s -> knit info e' f s
+ Inl e', s -> knit info tab e' f s
| Inr lam, s -> (lam,s))
| FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) ->
- (match ref_value_cache info (ConstKey c) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (ConstKey c) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
- (match ref_value_cache info (VarKey id) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (VarKey id) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FFlex(RelKey k) when red_set info.i_flags fDELTA ->
- (match ref_value_cache info (RelKey k) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (RelKey k) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FConstruct((ind,c),u) ->
let use_match = red_set info.i_flags fMATCH in
@@ -932,29 +934,29 @@ let rec knr info m stk =
| (depth, args, ZcaseT(ci,_,br,e)::s) when use_match ->
assert (ci.ci_npar>=0);
let rargs = drop_parameters depth ci.ci_npar args in
- knit info e br.(c-1) (rargs@s)
+ knit info tab e br.(c-1) (rargs@s)
| (_, cargs, Zfix(fx,par)::s) when use_fix ->
let rarg = fapp_stack(m,cargs) in
let stk' = par @ append_stack [|rarg|] s in
let (fxe,fxbd) = contract_fix_vect fx.term in
- knit info fxe fxbd stk'
+ knit info tab fxe fxbd stk'
| (depth, args, Zproj (n, m, cst)::s) when use_match ->
let rargs = drop_parameters depth n args in
let rarg = project_nth_arg m rargs in
- kni info rarg s
+ kni info tab rarg s
| (_,args,s) -> (m,args@s))
else (m,stk)
| FCoFix _ when red_set info.i_flags fCOFIX ->
(match strip_update_shift_app m stk with
(_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
let (fxe,fxbd) = contract_fix_vect m.term in
- knit info fxe fxbd (args@stk')
+ knit info tab fxe fxbd (args@stk')
| (_,args,s) -> (m,args@s))
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
- knit info (subs_cons([|v|],e)) bd stk
+ knit info tab (subs_cons([|v|],e)) bd stk
| FEvar(ev,env) ->
(match evar_value info.i_cache ev with
- Some c -> knit info env c stk
+ Some c -> knit info tab env c stk
| None -> (m,stk))
| FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
| FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
@@ -962,14 +964,14 @@ let rec knr info m stk =
(* Computes the weak head normal form of a term *)
-and kni info m stk =
+and kni info tab m stk =
let (hm,s) = knh info m stk in
- knr info hm s
-and knit info e t stk =
+ knr info tab hm s
+and knit info tab e t stk =
let (ht,s) = knht info e t stk in
- knr info ht s
+ knr info tab ht s
-let kh info v stk = fapp_stack(kni info v stk)
+let kh info tab v stk = fapp_stack(kni info tab v stk)
(************************************************************************)
@@ -997,61 +999,61 @@ let rec zip_term zfun m stk =
1- Calls kni
2- tries to rebuild the term. If a closure still has to be computed,
calls itself recursively. *)
-let rec kl info m =
+let rec kl info tab m =
if is_val m then (incr prune; term_of_fconstr m)
else
- let (nm,s) = kni info m [] in
+ let (nm,s) = kni info tab m [] in
let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
- zip_term (kl info) (norm_head info nm) s
+ zip_term (kl info tab) (norm_head info tab nm) s
(* no redex: go up for atoms and already normalized terms, go down
otherwise. *)
-and norm_head info m =
+and norm_head info tab m =
if is_val m then (incr prune; term_of_fconstr m) else
match m.term with
| FLambda(n,tys,f,e) ->
let (e',rvtys) =
List.fold_left (fun (e,ctxt) (na,ty) ->
- (subs_lift e, (na,kl info (mk_clos e ty))::ctxt))
+ (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt))
(e,[]) tys in
- let bd = kl info (mk_clos e' f) in
+ let bd = kl info tab (mk_clos e' f) in
List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys
| FLetIn(na,a,b,f,e) ->
let c = mk_clos (subs_lift e) f in
- mkLetIn(na, kl info a, kl info b, kl info c)
+ mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
| FProd(na,dom,rng) ->
- mkProd(na, kl info dom, kl info rng)
+ mkProd(na, kl info tab dom, kl info tab rng)
| FCoFix((n,(na,tys,bds)),e) ->
let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
- mkCoFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+ mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FFix((n,(na,tys,bds)),e) ->
let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
- mkFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+ mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FEvar((i,args),env) ->
- mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
+ mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
| FProj (p,c) ->
- mkProj (p, kl info c)
+ mkProj (p, kl info tab c)
| FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
| FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
(* Initialization and then normalization *)
(* weak reduction *)
-let whd_val info v =
- with_stats (lazy (term_of_fconstr (kh info v [])))
+let whd_val info tab v =
+ with_stats (lazy (term_of_fconstr (kh info tab v [])))
(* strong reduction *)
-let norm_val info v =
- with_stats (lazy (kl info v))
+let norm_val info tab v =
+ with_stats (lazy (kl info tab v))
let inject c = mk_clos (subs_id 0) c
-let whd_stack infos m stk =
- let k = kni infos m stk in
+let whd_stack infos tab m stk =
+ let k = kni infos tab m stk in
let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
k
@@ -1059,7 +1061,10 @@ let whd_stack infos m stk =
type clos_infos = fconstr infos
let create_clos_infos ?(evars=fun _ -> None) flgs env =
- create (fun _ -> inject) flgs env evars
+ create (fun _ _ c -> inject c) flgs env evars
+
+let create_tab () = KeyTable.create 17
+
let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
let env_of_infos infos = infos.i_cache.i_env
@@ -1067,14 +1072,14 @@ let env_of_infos infos = infos.i_cache.i_env
let infos_with_reds infos reds =
{ infos with i_flags = reds }
-let unfold_reference info key =
+let unfold_reference info tab key =
match key with
| ConstKey (kn,_) ->
if red_set info.i_flags (fCONST kn) then
- ref_value_cache info key
+ ref_value_cache info tab key
else None
| VarKey i ->
if red_set info.i_flags (fVAR i) then
- ref_value_cache info key
+ ref_value_cache info tab key
else None
- | _ -> ref_value_cache info key
+ | _ -> ref_value_cache info tab key
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b9c71d72af..3a7f77d521 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -100,13 +100,15 @@ val unfold_red : evaluable_global_reference -> reds
type table_key = Constant.t Univ.puniverses tableKey
type 'a infos_cache
+type 'a infos_tab
type 'a infos = {
i_flags : reds;
i_cache : 'a infos_cache }
-val ref_value_cache: 'a infos -> table_key -> 'a option
-val create: ('a infos -> constr -> 'a) -> reds -> env ->
+val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
+val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env ->
(existential -> constr option) -> 'a infos
+val create_tab : unit -> 'a infos_tab
val evar_value : 'a infos_cache -> existential -> constr option
val info_env : 'a infos -> env
@@ -200,15 +202,15 @@ val infos_with_reds : clos_infos -> reds -> clos_infos
(** Reduction function *)
(** [norm_val] is for strong normalization *)
-val norm_val : clos_infos -> fconstr -> constr
+val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
(** [whd_val] is for weak head normalization *)
-val whd_val : clos_infos -> fconstr -> constr
+val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
(** [whd_stack] performs weak head normalization in a given stack. It
stops whenever a reduction is blocked. *)
val whd_stack :
- clos_infos -> fconstr -> stack -> fconstr * stack
+ clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
to the conversion of the eta expansion of t, considered as an inhabitant
@@ -225,7 +227,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
(** Conversion auxiliary functions to do step by step normalisation *)
(** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> table_key -> fconstr option
+val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option
val eq_table_key : table_key -> table_key -> bool
@@ -241,9 +243,9 @@ val mk_clos_deep :
(fconstr subs -> constr -> fconstr) ->
fconstr subs -> constr -> fconstr
-val kni: clos_infos -> fconstr -> stack -> fconstr * stack
-val knr: clos_infos -> fconstr -> stack -> fconstr * stack
-val kl : clos_infos -> fconstr -> constr
+val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b3e6894143..2e59fcc18f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -117,12 +117,12 @@ let whd_betaiota env t =
| App (c, _) ->
begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t
- | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+ | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
end
- | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+ | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
let nf_betaiota env t =
- norm_val (create_clos_infos betaiota env) (inject t)
+ norm_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
let whd_betaiotazeta env x =
match kind x with
@@ -133,10 +133,10 @@ let whd_betaiotazeta env x =
| Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
| Case _ | Fix _ | CoFix _ | Proj _ ->
- whd_val (create_clos_infos betaiotazeta env) (inject x)
+ whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
end
| Rel _ | Cast _ | LetIn _ | Case _ | Proj _ ->
- whd_val (create_clos_infos betaiotazeta env) (inject x)
+ whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
let whd_all env t =
match kind t with
@@ -147,10 +147,10 @@ let whd_all env t =
| Ind _ | Construct _ | Evar _ | Meta _ -> t
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
| Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
- whd_val (create_clos_infos all env) (inject t)
+ whd_val (create_clos_infos all env) (create_tab ()) (inject t)
end
| Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ ->
- whd_val (create_clos_infos all env) (inject t)
+ whd_val (create_clos_infos all env) (create_tab ()) (inject t)
let whd_allnolet env t =
match kind t with
@@ -161,10 +161,10 @@ let whd_allnolet env t =
| Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
| Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
- whd_val (create_clos_infos allnolet env) (inject t)
+ whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
end
| Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ ->
- whd_val (create_clos_infos allnolet env) (inject t)
+ whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
(********************************************************************)
(* Conversion *)
@@ -316,46 +316,16 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
else raise NotConvertible
-let rec no_arg_available = function
- | [] -> true
- | Zupdate _ :: stk -> no_arg_available stk
- | Zshift _ :: stk -> no_arg_available stk
- | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk
- | Zproj _ :: _ -> true
- | ZcaseT _ :: _ -> true
- | Zfix _ :: _ -> true
-
-let rec no_nth_arg_available n = function
- | [] -> true
- | Zupdate _ :: stk -> no_nth_arg_available n stk
- | Zshift _ :: stk -> no_nth_arg_available n stk
- | Zapp v :: stk ->
- let k = Array.length v in
- if n >= k then no_nth_arg_available (n-k) stk
- else false
- | Zproj _ :: _ -> true
- | ZcaseT _ :: _ -> true
- | Zfix _ :: _ -> true
-
-let rec no_case_available = function
- | [] -> true
- | Zupdate _ :: stk -> no_case_available stk
- | Zshift _ :: stk -> no_case_available stk
- | Zapp _ :: stk -> no_case_available stk
- | Zproj (_,_,p) :: _ -> false
- | ZcaseT _ :: _ -> false
- | Zfix _ :: _ -> true
-
-let in_whnf (t,stk) =
- match fterm_of t with
- | (FLetIn _ | FCaseT _ | FApp _
- | FCLOS _ | FLIFT _ | FCast _) -> false
- | FLambda _ -> no_arg_available stk
- | FConstruct _ -> no_case_available stk
- | FCoFix _ -> no_case_available stk
- | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk
- | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
- | FLOCKED -> assert false
+type conv_tab = {
+ cnv_inf : clos_infos;
+ lft_tab : fconstr infos_tab;
+ rgt_tab : fconstr infos_tab;
+}
+(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
+ location contained both in tl and in tr. *)
+
+(** The same heap separation invariant must hold for the fconstr arguments
+ passed to each respective side of the conversion function below. *)
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
@@ -365,15 +335,10 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Control.check_for_interrupt ();
(* First head reduce both terms *)
- let whd = whd_stack (infos_with_reds infos betaiotazeta) in
- let rec whd_both (t1,stk1) (t2,stk2) =
- let st1' = whd t1 stk1 in
- let st2' = whd t2 stk2 in
- (* Now, whd_stack on term2 might have modified st1 (due to sharing),
- and st1 might not be in whnf anymore. If so, we iterate ccnv. *)
- if in_whnf st1' then (st1',st2') else whd_both st1' st2' in
- let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in
- let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in
+ let ninfos = infos_with_reds infos.cnv_inf betaiotazeta in
+ let (hd1, v1 as appr1) = whd_stack ninfos infos.lft_tab (fst st1) (snd st1) in
+ let (hd2, v2 as appr2) = whd_stack ninfos infos.rgt_tab (fst st2) (snd st2) in
+ let appr1 = (lft1, appr1) and appr2 = (lft2, appr2) in
(** We delay the computation of the lifts that apply to the head of the term
with [el_stack] inside the branches where they are actually used. *)
match (fterm_of hd1, fterm_of hd2) with
@@ -383,7 +348,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (Sort s1, Sort s2) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
- sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
+ sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -410,24 +375,24 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try
- let cuniv = conv_table_key infos fl1 fl2 cuniv in
+ let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with NotConvertible | Univ.UniverseInconsistency _ ->
(* else the oracle tells which constant is to be expanded *)
- let oracle = CClosure.oracle_of_infos infos in
+ let oracle = CClosure.oracle_of_infos infos.cnv_inf in
let (app1,app2) =
if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
- match unfold_reference infos fl1 with
+ match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 -> ((lft1, (def1, v1)), appr2)
| None ->
- (match unfold_reference infos fl2 with
+ (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 -> (appr1, (lft2, (def2, v2)))
| None -> raise NotConvertible)
else
- match unfold_reference infos fl2 with
+ match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 -> (appr1, (lft2, (def2, v2)))
| None ->
- (match unfold_reference infos fl1 with
+ (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 -> ((lft1, (def1, v1)), appr2)
| None -> raise NotConvertible)
in
@@ -437,11 +402,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* Projections: prefer unfolding to first-order unification,
which will happen naturally if the terms c1, c2 are not in constructor
form *)
- (match unfold_projection infos p1 with
+ (match unfold_projection infos.cnv_inf p1 with
| Some s1 ->
eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
| None ->
- match unfold_projection infos p2 with
+ match unfold_projection infos.cnv_inf p2 with
| Some s2 ->
eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
| None ->
@@ -455,26 +420,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
raise NotConvertible)
| (FProj (p1,c1), t2) ->
- (match unfold_projection infos p1 with
+ (match unfold_projection infos.cnv_inf p1 with
| Some s1 ->
eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
| None ->
(match t2 with
| FFlex fl2 ->
- (match unfold_reference infos fl2 with
+ (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 ->
eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
| None -> raise NotConvertible)
| _ -> raise NotConvertible))
| (t1, FProj (p2,c2)) ->
- (match unfold_projection infos p2 with
+ (match unfold_projection infos.cnv_inf p2 with
| Some s2 ->
eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
| None ->
(match t1 with
| FFlex fl1 ->
- (match unfold_reference infos fl1 with
+ (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 ->
eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
| None -> raise NotConvertible)
@@ -524,37 +489,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* only one constant, defined var or defined rel *)
| (FFlex fl1, c2) ->
- (match unfold_reference infos fl1 with
+ (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 ->
(** By virtue of the previous case analyses, we know [c2] is rigid.
Conversion check to rigid terms eventually implies full weak-head
reduction, so instead of repeatedly performing small-step
unfoldings, we perform reduction with all flags on. *)
- let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
- let r1 = whd_stack (infos_with_reds infos all) def1 v1 in
+ let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
+ let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in
eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
| None ->
match c2 with
| FConstruct ((ind2,j2),u2) ->
(try
let v2, v1 =
- eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
| (c1, FFlex fl2) ->
- (match unfold_reference infos fl2 with
+ (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 ->
(** Symmetrical case of above. *)
- let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
- let r2 = whd_stack (infos_with_reds infos all) def2 v2 in
+ let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
+ let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in
eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
| None ->
match c1 with
| FConstruct ((ind1,j1),u1) ->
(try let v1, v2 =
- eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
@@ -566,7 +531,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
- let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
+ let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
let nargs = CClosure.stack_args_size v1 in
if not (Int.equal nargs (CClosure.stack_args_size v2))
then raise NotConvertible
@@ -581,7 +546,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
- let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
+ let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
let nargs = CClosure.stack_args_size v1 in
if not (Int.equal nargs (CClosure.stack_args_size v2))
then raise NotConvertible
@@ -594,14 +559,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (FConstruct ((ind1,j1),u1), _) ->
(try
let v1, v2 =
- eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| (_, FConstruct ((ind2,j2),u2)) ->
(try
let v2, v1 =
- eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
@@ -669,6 +634,11 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
let infos = create_clos_infos ~evars reds env in
+ let infos = {
+ cnv_inf = infos;
+ lft_tab = create_tab ();
+ rgt_tab = create_tab ();
+ } in
ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
diff --git a/library/goptions.ml b/library/goptions.ml
index 5681421caa..76071ebcc2 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -196,7 +196,7 @@ type 'a option_sig = {
optread : unit -> 'a;
optwrite : 'a -> unit }
-type option_locality = OptLocal | OptDefault | OptGlobal
+type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
type option_mod = OptSet | OptAppend
@@ -229,11 +229,6 @@ let warn_deprecated_option =
(fun key -> str "Option" ++ spc () ++ str (nickname key) ++
strbrk " is deprecated")
-let get_locality = function
- | Some true -> OptLocal
- | Some false -> OptGlobal
- | None -> OptDefault
-
let declare_option cast uncast append ?(preprocess = fun x -> x)
{ optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
check_key key;
@@ -247,16 +242,30 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
match m with
| OptSet -> write v
| OptAppend -> write (append (read ()) v) in
- let load_options i o = cache_options o in
+ let load_options i (_, (l, _, _) as o) = match l with
+ | OptGlobal -> cache_options o
+ | OptExport -> ()
+ | OptLocal | OptDefault ->
+ (** Ruled out by classify_function *)
+ assert false
+ in
+ let open_options i (_, (l, _, _) as o) = match l with
+ | OptExport -> if Int.equal i 1 then cache_options o
+ | OptGlobal -> ()
+ | OptLocal | OptDefault ->
+ (** Ruled out by classify_function *)
+ assert false
+ in
let subst_options (subst,obj) = obj in
let discharge_options (_,(l,_,_ as o)) =
- match l with OptLocal -> None | _ -> Some o in
+ match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in
let classify_options (l,_,_ as o) =
- match l with OptGlobal -> Substitute o | _ -> Dispose in
+ match l with (OptExport | OptGlobal) -> Substitute o | (OptLocal | OptDefault) -> Dispose in
let options : option_locality * option_mod * _ -> obj =
declare_object
{ (default_object (nickname key)) with
load_function = load_options;
+ open_function = open_options;
cache_function = cache_options;
subst_function = subst_options;
discharge_function = discharge_options;
@@ -302,12 +311,12 @@ let warn_unknown_option =
(fun key -> strbrk "There is no option " ++
str (nickname key) ++ str ".")
-let set_option_value locality check_and_cast key v =
+let set_option_value ?(locality = OptDefault) check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
| Some (name, depr, (read,write,append)) ->
- write (get_locality locality) (check_and_cast v (read ()))
+ write locality (check_and_cast v (read ()))
let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
@@ -334,25 +343,25 @@ let check_unset_value v = function
warning. This allows a script to refer to an option that doesn't
exist anymore *)
-let set_int_option_value_gen locality =
- set_option_value locality check_int_value
-let set_bool_option_value_gen locality key v =
- set_option_value locality check_bool_value key v
-let set_string_option_value_gen locality =
- set_option_value locality check_string_value
-let unset_option_value_gen locality key =
- set_option_value locality check_unset_value key ()
+let set_int_option_value_gen ?locality =
+ set_option_value ?locality check_int_value
+let set_bool_option_value_gen ?locality key v =
+ set_option_value ?locality check_bool_value key v
+let set_string_option_value_gen ?locality =
+ set_option_value ?locality check_string_value
+let unset_option_value_gen ?locality key =
+ set_option_value ?locality check_unset_value key ()
-let set_string_option_append_value_gen locality key v =
+let set_string_option_append_value_gen ?(locality = OptDefault) key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
| Some (name, depr, (read,write,append)) ->
- append (get_locality locality) (check_string_value v (read ()))
+ append locality (check_string_value v (read ()))
-let set_int_option_value = set_int_option_value_gen None
-let set_bool_option_value = set_bool_option_value_gen None
-let set_string_option_value = set_string_option_value_gen None
+let set_int_option_value opt v = set_int_option_value_gen opt v
+let set_bool_option_value opt v = set_bool_option_value_gen opt v
+let set_string_option_value opt v = set_string_option_value_gen opt v
(* Printing options/tables *)
diff --git a/library/goptions.mli b/library/goptions.mli
index 31920b832a..6c14d19ee9 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -50,6 +50,8 @@ open Mod_subst
type option_name = string list
+type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
+
(** {6 Tables. } *)
(** The functor [MakeStringTable] declares a table containing objects
@@ -150,13 +152,12 @@ val get_ref_table :
mem : reference -> unit;
print : unit >
-(** The first argument is a locality flag.
- [Some true] = "Local", [Some false]="Global". *)
-val set_int_option_value_gen : bool option -> option_name -> int option -> unit
-val set_bool_option_value_gen : bool option -> option_name -> bool -> unit
-val set_string_option_value_gen : bool option -> option_name -> string -> unit
-val set_string_option_append_value_gen : bool option -> option_name -> string -> unit
-val unset_option_value_gen : bool option -> option_name -> unit
+(** The first argument is a locality flag. *)
+val set_int_option_value_gen : ?locality:option_locality -> option_name -> int option -> unit
+val set_bool_option_value_gen : ?locality:option_locality -> option_name -> bool -> unit
+val set_string_option_value_gen : ?locality:option_locality -> option_name -> string -> unit
+val set_string_option_append_value_gen : ?locality:option_locality -> option_name -> string -> unit
+val unset_option_value_gen : ?locality:option_locality -> option_name -> unit
val set_int_option_value : option_name -> int option -> unit
val set_bool_option_value : option_name -> bool -> unit
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index feaef31619..f1ec496231 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -822,7 +822,14 @@ GEXTEND Gram
END
GEXTEND Gram
- GLOBAL: command query_command class_rawexpr;
+ GLOBAL: command query_command class_rawexpr gallina_ext;
+
+ gallina_ext:
+ [ [ IDENT "Export"; "Set"; table = option_table; v = option_value ->
+ VernacSetOption (true, table, v)
+ | IDENT "Export"; IDENT "Unset"; table = option_table ->
+ VernacUnsetOption (true, table)
+ ] ];
command:
[ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
@@ -887,24 +894,9 @@ GEXTEND Gram
(* For acting on parameter tables *)
| "Set"; table = option_table; v = option_value ->
- begin match v with
- | StringValue s ->
- (* We make a special case for warnings because appending is their
- natural semantics *)
- if CString.List.equal table ["Warnings"] then
- VernacSetAppendOption (table, s)
- else
- let (last, prefix) = List.sep_last table in
- if String.equal last "Append" && not (List.is_empty prefix) then
- VernacSetAppendOption (prefix, s)
- else
- VernacSetOption (table, v)
- | _ -> VernacSetOption (table, v)
- end
- | "Set"; table = option_table ->
- VernacSetOption (table,BoolValue true)
+ VernacSetOption (false, table, v)
| IDENT "Unset"; table = option_table ->
- VernacUnsetOption table
+ VernacUnsetOption (false, table)
| IDENT "Print"; IDENT "Table"; table = option_table ->
VernacPrintOption table
@@ -1010,7 +1002,8 @@ GEXTEND Gram
| IDENT "Module"; qid = global -> LocateModule qid ] ]
;
option_value:
- [ [ n = integer -> IntValue (Some n)
+ [ [ -> BoolValue true
+ | n = integer -> IntValue (Some n)
| s = STRING -> StringValue s ] ]
;
option_ref_value:
@@ -1081,10 +1074,10 @@ GEXTEND Gram
(* Tactic Debugger *)
| IDENT "Debug"; IDENT "On" ->
- VernacSetOption (["Ltac";"Debug"], BoolValue true)
+ VernacSetOption (false, ["Ltac";"Debug"], BoolValue true)
| IDENT "Debug"; IDENT "Off" ->
- VernacSetOption (["Ltac";"Debug"], BoolValue false)
+ VernacSetOption (false, ["Ltac";"Debug"], BoolValue false)
(* registration of a custom reduction *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b6bac1a14e..99bb8440c6 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -90,7 +90,7 @@ let lookup_map map =
let protect_red map env sigma c0 =
let evars ev = Evarutil.safe_evar_value sigma ev in
let c = EConstr.Unsafe.to_constr c0 in
- EConstr.of_constr (kl (create_clos_infos ~evars all env)
+ EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ())
(mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));;
let protect_tac map =
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index e3941c1c5d..c3b6a7c59f 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -178,7 +178,7 @@ GEXTEND Gram
GLOBAL: gallina_ext;
gallina_ext:
[ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" ->
- Vernacexpr.VernacUnsetOption (["Printing"; "Implicit"; "Defensive"])
+ Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"])
] ]
;
END
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 7cfb30f4c1..a2155697ec 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -134,7 +134,7 @@ let mkSTACK = function
| STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk)
| v,stk -> STACK(0,v,stk)
-type cbv_infos = { infos : cbv_value infos; sigma : Evd.evar_map }
+type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map }
(* Change: zeta reduction cannot be avoided in CBV *)
@@ -318,7 +318,7 @@ let rec norm_head info env t stack =
and norm_head_ref k info env stack normt =
if red_set_ref (info_flags info.infos) normt then
- match ref_value_cache info.infos normt with
+ match ref_value_cache info.infos info.tab normt with
| Some body ->
if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
strip_appl (shift_value k body) stack
@@ -455,8 +455,8 @@ let cbv_norm infos constr =
(* constant bodies are normalized at the first expansion *)
let create_cbv_infos flgs env sigma =
let infos = create
- (fun old_info c -> cbv_stack_term { infos = old_info; sigma } TOP (subs_id 0) c)
+ (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c)
flgs
env
(Reductionops.safe_evar_value sigma) in
- { infos; sigma }
+ { tab = CClosure.create_tab (); infos; sigma }
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 20883f6f6b..eb283a0220 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -83,10 +83,12 @@ let infer_table_key infos variances c =
infer_generic_instance_eq variances u
| VarKey _ | RelKey _ -> variances
+let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk
+
let rec infer_fterm cv_pb infos variances hd stk =
Control.check_for_interrupt ();
- let open CClosure in
let hd,stk = whd_stack infos hd stk in
+ let open CClosure in
match fterm_of hd with
| FAtom a ->
begin match kind a with
@@ -116,7 +118,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
if Instance.is_empty u then variances
else
let nargs = stack_args_size stk in
- infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
+ infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u
in
infer_stack infos variances stk
| FConstruct (ctor,u) ->
@@ -124,7 +126,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
if Instance.is_empty u then variances
else
let nargs = stack_args_size stk in
- infer_constructor_instance_eq (info_env infos) variances ctor nargs u
+ infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u
in
infer_stack infos variances stk
| FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
@@ -161,7 +163,7 @@ and infer_vect infos variances v =
let infer_term cv_pb env variances c =
let open CClosure in
- let infos = create_clos_infos all env in
+ let infos = (create_clos_infos all env, create_tab ()) in
infer_fterm cv_pb infos variances (CClosure.inject c) []
let infer_arity_constructor is_arity env variances arcn =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 44a69d1c1e..0e66ff0b6f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1219,6 +1219,7 @@ let clos_norm_flags flgs env sigma t =
let evars ev = safe_evar_value sigma ev in
EConstr.of_constr (CClosure.norm_val
(CClosure.create_clos_infos ~evars flgs env)
+ (CClosure.create_tab ())
(CClosure.inject (EConstr.Unsafe.to_constr t)))
with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
@@ -1227,6 +1228,7 @@ let clos_whd_flags flgs env sigma t =
let evars ev = safe_evar_value sigma ev in
EConstr.of_constr (CClosure.whd_val
(CClosure.create_clos_infos ~evars flgs env)
+ (CClosure.create_tab ())
(CClosure.inject (EConstr.Unsafe.to_constr t)))
with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 542bf775fb..4c834f2f8f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -59,19 +59,21 @@ let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv =
let ar = inductive_type_knowing_parameters env !evdref ind argjv in
hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) }
| hj::restjl ->
- match EConstr.kind !evdref (whd_all env !evdref typ) with
- | Prod (_,c1,c2) ->
- if Evarconv.e_cumul env evdref hj.uj_type c1 then
- apply_rec (n+1) (subst1 hj.uj_val c2) restjl
- else
- error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
- | Evar ev ->
- let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
- evdref := evd';
- let (_,_,c2) = destProd evd' t in
- apply_rec (n+1) (subst1 hj.uj_val c2) restjl
- | _ ->
- error_cant_apply_not_functional env !evdref funj argjv
+ let (c1,c2) =
+ match EConstr.kind !evdref (whd_all env !evdref typ) with
+ | Prod (_,c1,c2) -> (c1,c2)
+ | Evar ev ->
+ let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
+ evdref := evd';
+ let (_,c1,c2) = destProd evd' t in
+ (c1,c2)
+ | _ ->
+ error_cant_apply_not_functional env !evdref funj argjv
+ in
+ if Evarconv.e_cumul env evdref hj.uj_type c1 then
+ apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+ else
+ error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
in
apply_rec 1 funj.uj_type (Array.to_list argjv)
@@ -81,19 +83,21 @@ let e_judge_of_apply env evdref funj argjv =
{ uj_val = mkApp (j_val funj, Array.map j_val argjv);
uj_type = typ }
| hj::restjl ->
- match EConstr.kind !evdref (whd_all env !evdref typ) with
- | Prod (_,c1,c2) ->
- if Evarconv.e_cumul env evdref hj.uj_type c1 then
- apply_rec (n+1) (subst1 hj.uj_val c2) restjl
- else
- error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
- | Evar ev ->
- let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
- evdref := evd';
- let (_,_,c2) = destProd evd' t in
- apply_rec (n+1) (subst1 hj.uj_val c2) restjl
- | _ ->
- error_cant_apply_not_functional env !evdref funj argjv
+ let (c1,c2) =
+ match EConstr.kind !evdref (whd_all env !evdref typ) with
+ | Prod (_,c1,c2) -> (c1,c2)
+ | Evar ev ->
+ let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
+ evdref := evd';
+ let (_,c1,c2) = destProd evd' t in
+ (c1,c2)
+ | _ ->
+ error_cant_apply_not_functional env !evdref funj argjv
+ in
+ if Evarconv.e_cumul env evdref hj.uj_type c1 then
+ apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+ else
+ error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
in
apply_rec 1 funj.uj_type (Array.to_list argjv)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2b7d643d6f..ea1ca26fbe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1118,18 +1118,15 @@ open Decl_kinds
hov 1 (keyword "Strategy" ++ spc() ++
hv 0 (prlist_with_sep sep pr_line l))
)
- | VernacUnsetOption (na) ->
+ | VernacUnsetOption (export, na) ->
+ let export = if export then keyword "Export" ++ spc () else mt () in
return (
- hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None)
+ hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None)
)
- | VernacSetOption (na,v) ->
+ | VernacSetOption (export, na,v) ->
+ let export = if export then keyword "Export" ++ spc () else mt () in
return (
- hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v)
- )
- | VernacSetAppendOption (na,v) ->
- return (
- hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++
- spc() ++ keyword "Append" ++ spc() ++ qs v)
+ hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v)
)
| VernacAddOption (na,l) ->
return (
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 48ccb8f4ce..f68c8b326b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -61,7 +61,7 @@ let classify_vernac e =
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
- | ( VernacSetOption (l,_) | VernacUnsetOption l)
+ | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
VtSideff [], VtNow
(* Qed *)
@@ -87,8 +87,8 @@ let classify_vernac e =
proof_block_detection = Some "curly" },
VtLater
(* Options changing parser *)
- | VernacUnsetOption (["Default";"Proof";"Using"])
- | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
+ | VernacUnsetOption (_, ["Default";"Proof";"Using"])
+ | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
@@ -149,7 +149,7 @@ let classify_vernac e =
| VernacReserve _
| VernacGeneralizable _
| VernacSetOpacity _ | VernacSetStrategy _
- | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _
+ | VernacUnsetOption _ | VernacSetOption _
| VernacAddOption _ | VernacRemoveOption _
| VernacMemOption _ | VernacPrintOption _
| VernacGlobalCheck _
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4c9b41b216..7764920d9f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1539,18 +1539,45 @@ let vernac_set_opacity ~atts (v,l) =
let l = List.map glob_ref l in
Redexpr.set_strategy local [v,l]
-let vernac_set_option ~atts key = function
- | StringValue s -> set_string_option_value_gen atts.locality key s
- | StringOptValue (Some s) -> set_string_option_value_gen atts.locality key s
- | StringOptValue None -> unset_option_value_gen atts.locality key
- | IntValue n -> set_int_option_value_gen atts.locality key n
- | BoolValue b -> set_bool_option_value_gen atts.locality key b
-
-let vernac_set_append_option ~atts key s =
- set_string_option_append_value_gen atts.locality key s
+let get_option_locality export local =
+ if export then
+ if Option.is_empty local then OptExport
+ else user_err Pp.(str "Locality modifiers forbidden with Export")
+ else match local with
+ | Some true -> OptLocal
+ | Some false -> OptGlobal
+ | None -> OptDefault
+
+let vernac_set_option0 ~atts export key opt =
+ let locality = get_option_locality export atts.locality in
+ match opt with
+ | StringValue s -> set_string_option_value_gen ~locality key s
+ | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
+ | StringOptValue None -> unset_option_value_gen ~locality key
+ | IntValue n -> set_int_option_value_gen ~locality key n
+ | BoolValue b -> set_bool_option_value_gen ~locality key b
+
+let vernac_set_append_option ~atts export key s =
+ let locality = get_option_locality export atts.locality in
+ set_string_option_append_value_gen ~locality key s
+
+let vernac_set_option ~atts export table v = match v with
+| StringValue s ->
+ (* We make a special case for warnings because appending is their
+ natural semantics *)
+ if CString.List.equal table ["Warnings"] then
+ vernac_set_append_option ~atts export table s
+ else
+ let (last, prefix) = List.sep_last table in
+ if String.equal last "Append" && not (List.is_empty prefix) then
+ vernac_set_append_option ~atts export prefix s
+ else
+ vernac_set_option0 ~atts export table v
+| _ -> vernac_set_option0 ~atts export table v
-let vernac_unset_option ~atts key =
- unset_option_value_gen atts.locality key
+let vernac_unset_option ~atts export key =
+ let locality = get_option_locality export atts.locality in
+ unset_option_value_gen ~locality key
let vernac_add_option key lv =
let f = function
@@ -2083,9 +2110,8 @@ let interp ?proof ~atts ~st c =
| VernacGeneralizable gen -> vernac_generalizable ~atts gen
| VernacSetOpacity qidl -> vernac_set_opacity ~atts qidl
| VernacSetStrategy l -> vernac_set_strategy ~atts l
- | VernacSetOption (key,v) -> vernac_set_option ~atts key v
- | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts key v
- | VernacUnsetOption key -> vernac_unset_option ~atts key
+ | VernacSetOption (export, key,v) -> vernac_set_option ~atts export key v
+ | VernacUnsetOption (export, key) -> vernac_unset_option ~atts export key
| VernacRemoveOption (key,v) -> vernac_remove_option key v
| VernacAddOption (key,v) -> vernac_add_option key v
| VernacMemOption (key,v) -> vernac_mem_option key v
@@ -2148,7 +2174,7 @@ let check_vernac_supports_locality c l =
| VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
| VernacGeneralizable _
| VernacSetOpacity _ | VernacSetStrategy _
- | VernacSetOption _ | VernacSetAppendOption _ | VernacUnsetOption _
+ | VernacSetOption _ | VernacUnsetOption _
| VernacDeclareReduction _
| VernacExtend _
| VernacInductive _) -> ()
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 44a7a9b15e..a837b77a33 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -52,7 +52,7 @@ let is_reset = function
| _ -> false
let is_debug cmd = match under_control cmd with
- | VernacSetOption (["Ltac";"Debug"], _) -> true
+ | VernacSetOption (_, ["Ltac";"Debug"], _) -> true
| _ -> false
let is_undo cmd = match under_control cmd with
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 16:03:35 +0000