diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 17 | ||||
| -rw-r--r-- | tactics/equality.ml | 49 | ||||
| -rw-r--r-- | tactics/equality.mli | 2 |
3 files changed, 46 insertions, 22 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 61f9c3b1c5..e093a27728 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -243,11 +243,16 @@ let get_roles export eff = in List.map map export +let feedback_axiom () = Feedback.(feedback AddedAxiom) +let is_unsafe_typing_flags () = + let flags = Environ.typing_flags (Global.env()) in + not (flags.check_universes && flags.check_guarded) + let define_constant ~side_effect ~name cd = let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let in_section = Lib.sections_are_opened () in - let export, decl = match cd with + let export, decl, unsafe = match cd with | DefinitionEntry de -> (* We deal with side effects *) if not de.proof_entry_opaque then @@ -257,19 +262,20 @@ let define_constant ~side_effect ~name cd = let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = Entries.DefinitionEntry (cast_proof_entry de) in - export, ConstantEntry (PureEntry, cd) + export, ConstantEntry (PureEntry, cd), false else let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain de.proof_entry_body map in let de = { de with proof_entry_body = body } in let de = cast_opaque_proof_entry de in - [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) + [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de), false | ParameterEntry e -> - [], ConstantEntry (PureEntry, Entries.ParameterEntry e) + [], ConstantEntry (PureEntry, Entries.ParameterEntry e), not (Lib.is_modtype_strict()) | PrimitiveEntry e -> - [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) + [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false in let kn, eff = Global.add_constant ~side_effect ~in_section name decl in + if unsafe || is_unsafe_typing_flags() then feedback_axiom(); kn, eff, export let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = @@ -489,6 +495,7 @@ let declare_mind mie = | ind::_ -> ind.mind_entry_typename | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive mie) in + if is_unsafe_typing_flags() then feedback_axiom(); let mind = Global.mind_of_delta_kn kn in let isprim = declare_projections mie.mind_entry_universes mind in Impargs.declare_mib_implicits mind; diff --git a/tactics/equality.ml b/tactics/equality.ml index 7c90c59f61..b9d718dd61 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -334,6 +334,21 @@ let jmeq_same_dom env sigma = function | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2 | _ -> false +let eq_elimination_ref l2r sort = + let name = + if l2r then + match sort with + | InProp -> "core.eq.ind_r" + | InSProp -> "core.eq.sind_r" + | InSet | InType -> "core.eq.rect_r" + else + match sort with + | InProp -> "core.eq.ind" + | InSProp -> "core.eq.sind" + | InSet | InType -> "core.eq.rect" + in + if Coqlib.has_ref name then Some (Coqlib.lib_ref name) else None + (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) @@ -345,35 +360,35 @@ let find_elim hdcncl lft2rgt dep cls ot = in let inccl = Option.is_empty cls in let env = Proofview.Goal.env gl in - (* if (is_global Coqlib.glob_eq hdcncl || *) - (* (is_global Coqlib.glob_jmeq hdcncl && *) - (* jmeq_same_dom env sigma ot)) && not dep *) - if (is_global_exists "core.eq.type" hdcncl || - (is_global_exists "core.JMeq.type" hdcncl - && jmeq_same_dom env sigma ot)) && not dep + let is_eq = is_global_exists "core.eq.type" hdcncl in + let is_jmeq = is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma ot in + if (is_eq || is_jmeq) && not dep then + let sort = elimination_sort_of_clause cls gl in let c = match EConstr.kind sigma hdcncl with | Ind (ind_sp,u) -> - let pr1 = - lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) - in begin match lft2rgt, cls with | Some true, None | Some false, Some _ -> - let c1 = destConstRef pr1 in - let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in - let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - begin + begin match if is_eq then eq_elimination_ref true sort else None with + | Some r -> destConstRef r + | None -> + let c1 = destConstRef (lookup_eliminator env ind_sp sort) in + let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in + let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in + let c1' = Global.constant_of_delta_kn (KerName.make mp l') in try - let _ = Global.lookup_constant c1' in - c1' + let _ = Global.lookup_constant c1' in c1' with Not_found -> user_err ~hdr:"Equality.find_elim" (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end - | _ -> destConstRef pr1 + | _ -> + begin match if is_eq then eq_elimination_ref false sort else None with + | Some r -> destConstRef r + | None -> destConstRef (lookup_eliminator env ind_sp sort) + end end | _ -> (* cannot occur since we checked that we are in presence of diff --git a/tactics/equality.mli b/tactics/equality.mli index f8166bba2d..8225195ca7 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -29,6 +29,8 @@ type conditions = | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *) +val eq_elimination_ref : orientation -> Sorts.family -> GlobRef.t option + val general_rewrite_bindings : orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> evars_flag -> unit Proofview.tactic |