From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 24 Mar 2017 02:18:53 +0100 Subject: A fix to #5414 (ident bound by ltac names now known for "match"). Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let". --- plugins/funind/glob_termops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index eae72d9e84..1f2a0a1b4d 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -722,7 +722,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* we first (pseudo) understand [rt] and get back the computed evar_map *) (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) - let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Pretyping.empty_lvar expected_type rt in + let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in let ctx, f = Evarutil.nf_evars_and_universes ctx in (* then we map [rt] to replace the implicit holes by their values *) -- cgit v1.2.3 From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Jun 2017 06:08:02 +0200 Subject: [proof] Deprecate redundant wrappers. As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. --- plugins/funind/functional_principles_types.ml | 8 ++++---- plugins/funind/indfun_common.ml | 4 ++-- plugins/funind/recdef.ml | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index fd4b52b65c..de5a5685b5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -371,12 +371,12 @@ let generate_functional_principle (evd: Evd.evar_map ref) begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () @@ -524,12 +524,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8f62231aeb..b824c3e293 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -161,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook = let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in - if with_clean then Pfedit.delete_current_proof (); + if with_clean then Proof_global.discard_current (); CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id @@ -173,7 +173,7 @@ let cook_proof _ = let get_proof_clean do_reduce = let result = cook_proof do_reduce in - Pfedit.delete_current_proof (); + Proof_global.discard_current (); result let with_full_print f a = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index bd74d2cf64..b1c69812dc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1295,7 +1295,7 @@ let is_opaque_constant c = let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = get_current_proof_name () in + let current_proof_name = Proof_global.get_current_proof_name () in let name = match goal_name with | Some s -> s | None -> -- cgit v1.2.3 From 27c8e30fad95d887b698b0e3fa563644c293b033 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 23 Jun 2016 15:07:02 +0200 Subject: Prelude : no more autoload of plugins extraction and recdef The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. --- plugins/funind/FunInd.v | 10 ++++++++++ plugins/funind/Recdef.v | 2 +- 2 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 plugins/funind/FunInd.v (limited to 'plugins/funind') diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v new file mode 100644 index 0000000000..e40aea7764 --- /dev/null +++ b/plugins/funind/FunInd.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* let _time3 = System.get_time () in @@ -1470,7 +1472,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1485,7 +1487,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c75f7f868c..ba88563d3b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -880,7 +880,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,pl,impls = Command.interp_mutual_inductive indl [] - false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in + false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) -- cgit v1.2.3 From 0437339ccac602d692b5b8c071b77ac756805520 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Jun 2017 16:41:09 +0200 Subject: Removing Proof_type from the API. Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead. --- plugins/funind/functional_principles_proofs.ml | 3 +-- plugins/funind/functional_principles_proofs.mli | 4 ++-- plugins/funind/functional_principles_types.mli | 2 +- plugins/funind/indfun.ml | 4 ++-- plugins/funind/indfun.mli | 2 +- plugins/funind/indfun_common.mli | 4 ++-- plugins/funind/invfun.ml | 10 +++++----- plugins/funind/recdef.ml | 2 +- plugins/funind/recdef.mli | 4 ++-- 9 files changed, 17 insertions(+), 18 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef894b2395..ba46f78aa8 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -10,7 +10,6 @@ open Names open Pp open Tacmach open Termops -open Proof_type open Tacticals open Tactics open Indfun_common @@ -106,7 +105,7 @@ let make_refl_eq constructor type_of_t t = type pte_info = { - proving_tac : (Id.t list -> Proof_type.tactic); + proving_tac : (Id.t list -> Tacmach.tactic); is_valid : constr -> bool } diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 5bb288678d..d03fc475e0 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -4,7 +4,7 @@ open Names val prove_princ_for_struct : Evd.evar_map ref -> bool -> - int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic + int -> Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic val prove_principle_for_gen : @@ -14,7 +14,7 @@ val prove_principle_for_gen : int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) EConstr.constr -> (* the wf relation used to prove the function *) - Proof_type.tactic + Tacmach.tactic (* val is_pte : rel_declaration -> bool *) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index bb2b2d9186..e70ef23656 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -28,7 +28,7 @@ val generate_functional_principle : (* The tactic to use to make the proof w.r the number of params *) - (EConstr.constr array -> int -> Proof_type.tactic) -> + (EConstr.constr array -> int -> Tacmach.tactic) -> unit val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d12aa7f425..ad04e430cd 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -343,7 +343,7 @@ let error_error names e = let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> - Proof_type.tactic) : unit = + Tacmach.tactic) : unit = let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in @@ -446,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation - (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic = + (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 33420d8132..fc7da6a338 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -16,7 +16,7 @@ val functional_induction : EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> Tacexpr.or_and_intro_pattern option -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val make_graph : Globnames.global_reference -> unit diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 6b40c91713..f7a9cedd73 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -105,7 +105,7 @@ exception ToShow of exn val is_strict_tcc : unit -> bool -val h_intros: Names.Id.t list -> Proof_type.tactic +val h_intros: Names.Id.t list -> Tacmach.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed @@ -114,7 +114,7 @@ val well_founded_ltof : EConstr.constr Util.delayed val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference -val list_rewrite : bool -> (EConstr.constr*bool) list -> Proof_type.tactic +val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ebdb490e37..94ef2590c8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -218,7 +218,7 @@ let rec generate_fresh_id x avoid i = \end{enumerate} *) -let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Proof_type.tactic = +let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -468,7 +468,7 @@ let tauto = let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g -and intros_with_rewrite_aux : Proof_type.tactic = +and intros_with_rewrite_aux : Tacmach.tactic = fun g -> let eq_ind = make_eq () in let sigma = project g in @@ -629,7 +629,7 @@ let rec reflexivity_with_destruct_cases g = *) -let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.tactic = +let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* We compute the types of the different mutually recursive lemmas in $\zeta$ normal form @@ -673,7 +673,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.ta using [f_equation] if it is recursive (that is the graph is infinite or unfold if the graph is finite *) - let rewrite_tac j ids : Proof_type.tactic = + let rewrite_tac j ids : Tacmach.tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) @@ -953,7 +953,7 @@ let revert_graph kn post_tac hid g = \end{enumerate} *) -let functional_inversion kn hid fconst f_correct : Proof_type.tactic = +let functional_inversion kn hid fconst f_correct : Tacmach.tactic = fun g -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let sigma = project g in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3cd20a9507..8e12b239e8 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -30,7 +30,7 @@ open Nametab open Declare open Decl_kinds open Tacred -open Proof_type +open Goal open Pfedit open Glob_term open Pretyping diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index e1a072799e..f3d5e73320 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -2,10 +2,10 @@ open API (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : - Proof_type.tactic -> + Tacmach.tactic -> bool -> Names.Id.t list option -> - Proof_type.tactic + Tacmach.tactic val recursive_definition : bool -> Names.Id.t -> -- cgit v1.2.3 From 181cb78d09ba55c7a6d62b333b26595a4fbb360a Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Fri, 23 Jun 2017 15:06:49 +0200 Subject: closing bug #4250 --- plugins/funind/indfun.ml | 78 ++++++++++++++++++++++-------------------------- 1 file changed, 36 insertions(+), 42 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ad04e430cd..35f0929587 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -576,50 +576,44 @@ let map_option f = function | Some v -> Some (f v) open Constrexpr -open Topconstr -let make_assoc assoc l1 l2 = - let fold assoc a b = match a, b with - | (_, Name na), (_, Name id) -> Id.Map.add na id assoc - | _, _ -> assoc - in - List.fold_left2 fold assoc l1 l2 - -let rec rebuild_bl (aux,assoc) bl typ = - match bl,typ with - | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) - | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> - rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } -> - rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) +let rec rebuild_bl aux bl typ = + match bl,typ with + | [], _ -> List.rev aux,typ + | (CLocalAssum(nal,bk,_))::bl',typ -> + rebuild_nal aux bk bl' nal typ + | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } -> + rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux) bl' typ' | _ -> assert false - and rebuild_nal (aux,assoc) bk bl' nal lnal typ = - match nal, typ.CAst.v with - | [], _ -> rebuild_bl (aux,assoc) bl' typ - | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ - | _,CProdN((nal',bk',nal't)::rest,typ') -> - let lnal' = List.length nal' in - if lnal' >= lnal - then - let old_nal',new_nal' = List.chop lnal nal' in - let nassoc = make_assoc assoc old_nal' nal in - let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in - rebuild_bl ((assum :: aux), nassoc) bl' - (if List.is_empty new_nal' && List.is_empty rest - then typ' - else CAst.make @@ if List.is_empty new_nal' - then CProdN(rest,typ') - else CProdN(((new_nal',bk',nal't)::rest),typ')) - else - let captured_nal,non_captured_nal = List.chop lnal' nal in - let nassoc = make_assoc assoc nal' captured_nal in - let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in - rebuild_nal ((assum :: aux), nassoc) - bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ')) - | _ -> assert false - -let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ +and rebuild_nal aux bk bl' nal typ = + match nal,typ with + | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ + | [], _ -> rebuild_bl aux bl' typ + | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> + if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') + then + let assum = CLocalAssum([na],bk',nal't) in + let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + nal + (CAst.make @@ CProdN(new_rest,typ')) + else + let assum = CLocalAssum([na'],bk',nal't) in + let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + (na::nal) + (CAst.make @@ CProdN(new_rest,typ')) + | _ -> + assert false + +let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in @@ -629,7 +623,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> - let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) bl fix_typ in + let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixpoint_exprl constr_expr_typel -- cgit v1.2.3 From 10c81e90a836c8abea32bc6157976b9adf7775fa Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Thu, 29 Jun 2017 17:27:04 +0200 Subject: closing bug #5618 introduce by PR 828 --- plugins/funind/indfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 35f0929587..2c5dae1cde 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -593,7 +593,7 @@ and rebuild_nal aux bk bl' nal typ = | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') then - let assum = CLocalAssum([na],bk',nal't) in + let assum = CLocalAssum([na],bk,nal't) in let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in rebuild_nal (assum::aux) @@ -602,7 +602,7 @@ and rebuild_nal aux bk bl' nal typ = nal (CAst.make @@ CProdN(new_rest,typ')) else - let assum = CLocalAssum([na'],bk',nal't) in + let assum = CLocalAssum([na'],bk,nal't) in let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in rebuild_nal (assum::aux) -- cgit v1.2.3