diff options
Diffstat (limited to 'plugins')
25 files changed, 284 insertions, 83 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index f503c572d0..3c46d5c43b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -342,7 +342,7 @@ let rec extract_structure env mp reso ~all = function and extract_mexpr env mp = function | MEwith _ -> assert false (* no 'with' syntax for modules *) - | me when lang () != Ocaml -> + | me when lang () != Ocaml || Table.is_extrcompute () -> (* In Haskell/Scheme, we expand everything. For now, we also extract everything, dead code will be removed later (see [Modutil.optimize_struct]. *) @@ -570,11 +570,12 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init modular library = +let init ?(compute=false) modular library = check_inside_section (); check_inside_module (); set_keywords (descr ()).keywords; set_modular modular; set_library library; + set_extrcompute compute; reset (); if modular && lang () == Scheme then error_scheme () @@ -684,8 +685,22 @@ let extraction_library is_rec m = List.iter print struc; reset () +(** For extraction compute, we flatten all the module structure, + getting rid of module types or unapplied functors *) + +let flatten_structure struc = + let rec flatten_elem (lab,elem) = match elem with + |SEdecl d -> [d] + |SEmodtype _ -> [] + |SEmodule m -> match m.ml_mod_expr with + |MEfunctor _ -> [] + |MEident _ | MEapply _ -> assert false (* should be expanded *) + |MEstruct (_,elems) -> flatten_elems elems + and flatten_elems l = List.flatten (List.map flatten_elem l) + in flatten_elems (List.flatten (List.map snd struc)) + let structure_for_compute c = - init false false; + init false false ~compute:true; let env = Global.env () in let ast, mlt = Extraction.extract_constr env c in let ast = Mlutil.normalize ast in @@ -694,8 +709,7 @@ let structure_for_compute c = let () = ast_iter_references add_ref add_ref add_ref ast in let refs = Refset.elements !refs in let struc = optimize_struct (refs,[]) (mono_environment refs []) in - let flatstruc = List.map snd (List.flatten (List.map snd struc)) in - flatstruc, ast, mlt + (flatten_structure struc), ast, mlt (* For the test-suite : extraction to a temporary file + run ocamlc on it *) diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 5769ff1176..7bbb825b10 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -34,5 +34,4 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Term.constr -> - Miniml.ml_flat_structure * Miniml.ml_ast * Miniml.ml_type + Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index edebba49df..5e967ef379 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -187,8 +187,6 @@ type ml_structure = (ModPath.t * ml_module_structure) list type ml_signature = (ModPath.t * ml_module_sig) list -type ml_flat_structure = ml_structure_elem list - type unsafe_needs = { mldummy : bool; tdummy : bool; diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a4c2bcd883..b01b0198d5 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -127,11 +127,15 @@ let rec mgu = function | Taxiom, Taxiom -> () | _ -> raise Impossible -let needs_magic p = try mgu p; false with Impossible -> true +let skip_typing () = lang () == Scheme || is_extrcompute () -let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a +let needs_magic p = + if skip_typing () then false + else try mgu p; false with Impossible -> true -let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a +let put_magic_if b a = if b then MLmagic a else a + +let put_magic p a = if needs_magic p then MLmagic a else a let generalizable a = lang () != Ocaml || @@ -769,6 +773,20 @@ let eta_red e = else e | _ -> e +(* Performs an eta-reduction when the core is atomic, + or otherwise returns None *) + +let atomic_eta_red e = + let ids,t = collect_lams e in + let n = List.length ids in + match t with + | MLapp (f,a) when test_eta_args_lift 0 n a -> + (match f with + | MLrel k when k>n -> Some (MLrel (k-n)) + | MLglob _ | MLexn _ | MLdummy _ -> Some f + | _ -> None) + | _ -> None + (*s Computes all head linear beta-reductions possible in [(t a)]. Non-linear head beta-redex become let-in. *) @@ -1053,6 +1071,10 @@ let rec simpl o = function simpl o (MLcase(typ,e,br')) | MLmagic(MLdummy _ as e) when lang () == Haskell -> e | MLmagic(MLexn _ as e) -> e + | MLlam _ as e -> + (match atomic_eta_red e with + | Some e' -> e' + | None -> ast_map (simpl o) e) | a -> ast_map (simpl o) a (* invariant : list [a] of arguments is non-empty *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 30e3b520f9..995d5fd19d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -250,6 +250,11 @@ let modular () = !modular_ref let set_library b = library_ref := b let library () = !library_ref +let extrcompute = ref false + +let set_extrcompute b = extrcompute := b +let is_extrcompute () = !extrcompute + (*s Printing. *) (* The following functions work even on objects not in [Global.env ()]. diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7e47d0bc81..cc93f294b3 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -165,6 +165,9 @@ val modular : unit -> bool val set_library : bool -> unit val library : unit -> bool +val set_extrcompute : bool -> unit +val is_extrcompute : unit -> bool + (*s Table for custom inlining *) val to_inline : global_reference -> bool diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 86c983bdd9..d639dd0e1c 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -482,6 +482,11 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ] END +VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY +| [ "Locate" "Ltac" reference(r) ] -> + [ Tacentries.print_located_tactic r ] +END + let pr_ltac_ref = Libnames.pr_reference let pr_tacdef_body tacdef_body = diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack index 12b4c81fc4..3972b7aac3 100644 --- a/plugins/ltac/ltac_plugin.mlpack +++ b/plugins/ltac/ltac_plugin.mlpack @@ -1,9 +1,9 @@ Tacarg +Tacsubst +Tacenv Pptactic Pltac Taccoerce -Tacsubst -Tacenv Tactic_debug Tacintern Tacentries diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d8bd166208..d588c888c4 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -336,7 +336,7 @@ type 'a extra_genarg_printer = let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn else try - pr_qualid (Nametab.shortest_qualid_of_tactic kn) + pr_qualid (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) str "<" ++ KerName.print kn ++ str ">" diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index c79d5b389f..d9da954fe6 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -93,7 +93,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t val pr_alias : (Val.t -> Pp.t) -> int -> Names.KerName.t -> Val.t list -> Pp.t -val pr_ltac_constant : Nametab.ltac_constant -> Pp.t +val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : raw_tactic_expr -> Pp.t diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 32494a8793..9ae8bfe65b 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -367,18 +367,30 @@ let do_profile s call_trace tac = let get_local_profiling_results () = List.hd Local.(!stack) -module SM = Map.Make(Stateid.Self) +(* We maintain our own cache of document data, given that the + semantics of the STM implies that synchronized state for opaque + proofs will be lost on QED. This provides some complications later + on as we will have to simulate going back on the document on our + own. *) +module DData = struct + type t = Feedback.doc_id * Stateid.t + let compare x y = Pervasives.compare x y +end + +module SM = Map.Make(DData) let data = ref SM.empty let _ = Feedback.(add_feeder (function - | { id = s; contents = Custom (_, "ltacprof_results", xml) } -> + | { doc_id = d; + span_id = s; + contents = Custom (_, "ltacprof_results", xml) } -> let results = to_ltacprof_results xml in let other_results = (* Multi success can cause this *) - try SM.find s !data + try SM.find (d,s) !data with Not_found -> empty_treenode root in - data := SM.add s (merge_roots results other_results) !data + data := SM.add (d,s) (merge_roots results other_results) !data | _ -> ())) let reset_profile () = @@ -388,7 +400,10 @@ let reset_profile () = (* ******************** *) let print_results_filter ~cutoff ~filter = - let valid id _ = Stm.state_of_id id <> `Expired in + (* The STM doesn't provide yet a proper document query and traversal + API, thus we need to re-check if some states are current anymore + (due to backtracking) using the `state_of_id` API. *) + let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in data := SM.filter valid !data; let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fd791a9101..1809f0fcdb 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1935,7 +1935,12 @@ let default_morphism sign m = let evars, mor = resolve_one_typeclass env (goalevars evars) morph in mor, proper_projection sigma mor morph +let warn_add_setoid_deprecated = + CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> + Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) + let add_setoid global binders a aeq t n = + warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in @@ -1954,7 +1959,12 @@ let make_tactic name = let tacname = Qualid (Loc.tag tacpath) in TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, []))) +let warn_add_morphism_deprecated = + CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> + Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) + let add_morphism_infer glob m n = + warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a8d518fbd8..bcd5b388a1 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -409,7 +409,7 @@ let create_ltac_quotation name cast (e, l) = type tacdef_kind = | NewTac of Id.t - | UpdateTac of Nametab.ltac_constant + | UpdateTac of Tacexpr.ltac_constant let is_defined_tac kn = try ignore (Tacenv.interp_ltac kn); true with Not_found -> false @@ -441,7 +441,7 @@ let register_ltac local tacl = | Tacexpr.TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in let kn = - try Nametab.locate_tactic (snd (qualid_of_reference ident)) + try Tacenv.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> CErrors.user_err ?loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") @@ -464,7 +464,7 @@ let register_ltac local tacl = let defs () = (** Register locally the tactic to handle recursivity. This function affects the whole environment, so that we transactify it afterwards. *) - let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in + let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in let () = List.iter iter_rec recvars in List.map map rfun in @@ -475,7 +475,7 @@ let register_ltac local tacl = Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> Tacenv.redefine_ltac local kn tac; - let name = Nametab.shortest_qualid_of_tactic kn in + let name = Tacenv.shortest_qualid_of_tactic kn in Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") in List.iter iter defs @@ -488,7 +488,7 @@ let print_ltacs () = let entries = List.sort sort entries in let map (kn, entry) = let qid = - try Some (Nametab.shortest_qualid_of_tactic kn) + try Some (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> None in match qid with @@ -506,6 +506,31 @@ let print_ltacs () = in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) +let locatable_ltac = "Ltac" + +let () = + let open Prettyp in + let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in + let locate_all = Tacenv.locate_extended_all_tactic in + let shortest_qualid = Tacenv.shortest_qualid_of_tactic in + let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in + let print kn = + let qid = qualid_of_path (Tacenv.path_of_tactic kn) in + Tacintern.print_ltac qid + in + let about = name in + register_locatable locatable_ltac { + locate; + locate_all; + shortest_qualid; + name; + print; + about; + } + +let print_located_tactic qid = + Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid) + (** Grammar *) let () = diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index aa8f4efe65..ab2c6b3073 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -62,3 +62,6 @@ val create_ltac_quotation : string -> val print_ltacs : unit -> unit (** Display the list of ltac definitions currently available. *) + +val print_located_tactic : Libnames.reference -> unit +(** Display the absolute name of a tactic. *) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 13b44f0e2c..8c59a36fa6 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -11,6 +11,42 @@ open Pp open Names open Tacexpr +(** Nametab for tactics *) + +(** TODO: Share me somewhere *) +module FullPath = +struct + open Libnames + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (DirPath.repr dir) +end + +module KnTab = Nametab.Make(FullPath)(KerName) + +let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty) + +let push_tactic vis sp kn = + let (tab, revtab) = !tactic_tab in + let tab = KnTab.push vis sp kn tab in + let revtab = KNmap.add kn sp revtab in + tactic_tab := (tab, revtab) + +let locate_tactic qid = KnTab.locate qid (fst !tactic_tab) + +let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab) + +let exists_tactic kn = KnTab.exists kn (fst !tactic_tab) + +let path_of_tactic kn = KNmap.find kn (snd !tactic_tab) + +let shortest_qualid_of_tactic kn = + let sp = KNmap.find kn (snd !tactic_tab) in + KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab) + (** Tactic notations (TacAlias) *) type alias = KerName.t @@ -103,19 +139,19 @@ let replace kn path t = let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Until i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t)) = match id with | None -> - let () = if not local then Nametab.push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Exactly i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> - let () = Nametab.push_tactic (Until 1) sp kn in + let () = push_tactic (Until 1) sp kn in add kn b t | Some kn0 -> replace kn0 kn t @@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) = let classify_md (local, _, _, _ as o) = Substitute o -let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 958109e5a7..4ecc978fea 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -7,11 +7,21 @@ (************************************************************************) open Names +open Libnames open Tacexpr open Geninterp (** This module centralizes the various ways of registering tactics. *) +(** {5 Tactic naming} *) + +val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit +val locate_tactic : qualid -> ltac_constant +val locate_extended_all_tactic : qualid -> ltac_constant list +val exists_tactic : full_path -> bool +val path_of_tactic : ltac_constant -> full_path +val shortest_qualid_of_tactic : ltac_constant -> qualid + (** {5 Tactic notations} *) type alias = KerName.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 64da097deb..2c36faeff4 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -10,13 +10,14 @@ open Loc open Names open Constrexpr open Libnames -open Nametab open Genredexpr open Genarg open Pattern open Misctypes open Locus +type ltac_constant = KerName.t + type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index fc6ee6aab6..99d7684d36 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -118,7 +118,7 @@ let intern_constr_reference strict ist = function let intern_isolated_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[])) + TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) @@ -137,7 +137,7 @@ let intern_isolated_tactic_reference strict ist r = let intern_applied_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - ArgArg (loc,locate_tactic qid) + ArgArg (loc,Tacenv.locate_tactic qid) let intern_applied_tactic_reference ist r = (* An ltac reference *) @@ -722,7 +722,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try - let kn = Nametab.locate_tactic id in + let kn = Tacenv.locate_tactic id in let entries = Tacenv.ltac_entries () in let tac = KNmap.find kn entries in let filter mp = diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 56b3d480eb..ae4857a77c 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -56,10 +56,18 @@ Section MakeRingPol. Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (* Useful tactics *) - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 56b985aa34..88e2cb1da5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -56,11 +56,16 @@ Let rI_neq_rO := AFth.(AF_1_neq_0). Let rdiv_def := AFth.(AFdiv_def). Let rinv_l := AFth.(AFinv_l). -Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed. -Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed. -Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed. -Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. -Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed. +Add Morphism radd with signature (req ==> req ==> req) as radd_ext. +Proof. exact (Radd_ext Reqe). Qed. +Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. +Proof. exact (Rmul_ext Reqe). Qed. +Add Morphism ropp with signature (req ==> req) as ropp_ext. +Proof. exact (Ropp_ext Reqe). Qed. +Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. +Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. +Add Morphism rinv with signature (req ==> req) as rinv_ext. +Proof. exact SRinv_ext. Qed. Let eq_trans := Setoid.Seq_trans _ _ Rsth. Let eq_sym := Setoid.Seq_sym _ _ Rsth. @@ -1609,9 +1614,12 @@ Section Complete. Variable Rsth : Setoid_Theory R req. Add Setoid R req Rsth as R_setoid3. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext3. + Proof. exact (Ropp_ext Reqe). Qed. Section AlmostField. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 98ffff4322..bd4e94687d 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -51,9 +51,12 @@ Section ZMORPHISM. Add Setoid R req Rsth as R_setoid3. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext3. + Proof. exact (Ropp_ext Reqe). Qed. Fixpoint gen_phiPOS1 (p:positive) : R := match p with @@ -103,7 +106,8 @@ Section ZMORPHISM. Section ALMOST_RING. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -151,7 +155,8 @@ Section ZMORPHISM. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. Let ARth := Rth_ARth Rsth Reqe Rth. - Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -265,8 +270,10 @@ Section NMORPHISM. Let rsub := (@SRsub R radd). Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). - Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext4. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4. + Proof. exact (Rmul_ext Reqe). Qed. Ltac norm := gen_srewrite_sr Rsth Reqe ARth. Definition gen_phiN1 x := @@ -377,12 +384,16 @@ Section NWORDMORPHISM. Add Setoid R req Rsth as R_setoid5. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext5. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext5. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext5. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext5. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext5. + Proof. exact (Ropp_ext Reqe). Qed. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -557,10 +568,14 @@ Section GEN_DIV. (* Useful tactics *) Add Setoid R req Rsth as R_set1. Ltac rrefl := gen_reflexivity Rsth. - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Definition triv_div x y := @@ -859,8 +874,3 @@ Ltac isZcst t := (* *) | _ => constr:(false) end. - - - - - diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index ac54d862c9..a94f8d8df6 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -59,10 +59,18 @@ Section MakeRingPol. Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (* Useful tactics *) - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 8dda5ecd34..335a68d70f 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -254,8 +254,12 @@ Section ALMOST_RING. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. - Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. - Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext1. + Proof. exact (SRadd_ext SReqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext1. + Proof. exact (SRmul_ext SReqe). Qed. + Variable SRth : semi_ring_theory 0 1 radd rmul req. (** Every semi ring can be seen as an almost ring, by taking : @@ -323,9 +327,15 @@ Section ALMOST_RING. Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed. + + Add Morphism radd with signature (req ==> req ==> req) as radd_ext2. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext2. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext2. + Proof. exact (Ropp_ext Reqe). Qed. Section RING. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. @@ -393,14 +403,25 @@ Section ALMOST_RING. Notation "?=!" := ceqb. Notation "[ x ]" := (phi x). Variable Csth : Equivalence ceq. Variable Ceqe : ring_eq_ext cadd cmul copp ceq. + Add Setoid C ceq Csth as C_setoid. - Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. - Add Morphism cmul : cmul_ext. exact (Rmul_ext Ceqe). Qed. - Add Morphism copp : copp_ext. exact (Ropp_ext Ceqe). Qed. + + Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext. + Proof. exact (Radd_ext Ceqe). Qed. + + Add Morphism cmul with signature (ceq ==> ceq ==> ceq) as cmul_ext. + Proof. exact (Rmul_ext Ceqe). Qed. + + Add Morphism copp with signature (ceq ==> ceq) as copp_ext. + Proof. exact (Ropp_ext Ceqe). Qed. + Variable Cth : ring_theory cO cI cadd cmul csub copp ceq. Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi. Variable phi_ext : forall x y, ceq x y -> [x] == [y]. - Add Morphism phi : phi_ext1. exact phi_ext. Qed. + + Add Morphism phi with signature (ceq ==> req) as phi_ext1. + Proof. exact phi_ext. Qed. + Lemma Smorph_opp x : [-!x] == -[x]. Proof. rewrite <- (Rth.(Radd_0_l) [-!x]). diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index cf5fdf3184..d37c676e38 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -814,8 +814,8 @@ let ssr_n_tac seed n gl = let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in let fail msg = CErrors.user_err (Pp.str msg) in let tacname = - try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) - with Not_found -> try Nametab.locate_tactic (ssrqid name) + try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) + with Not_found -> try Tacenv.locate_tactic (ssrqid name) with Not_found -> if n = -1 then fail "The ssreflect library was not loaded" else fail ("The tactic "^name^" was not found") in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 1e1a986daa..7b591feada 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1554,8 +1554,8 @@ END let ssrautoprop gl = try let tacname = - try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) - with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in + try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) + with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl |