From d1372d531ff912fe726ed4a79ac556d378a37375 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 3 Sep 2008 14:45:58 +0000 Subject: Fix bug #1935, reworking the reflexivity, symmetry... tactics to use the same typeclass method application tactic that's available to users. Modify a bit the _red tactics to accomodate the new setup and comment some dead code in setoid_replace. Next step is removing it completely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11355 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/class_tactics.ml4 | 226 ++++++++++++++++++++++++++++----------------- tactics/setoid_replace.ml | 156 +++++++++++++++---------------- tactics/setoid_replace.mli | 8 +- tactics/tacinterp.mli | 7 ++ tactics/tactics.ml | 41 ++++---- tactics/tactics.mli | 6 +- 6 files changed, 260 insertions(+), 184 deletions(-) (limited to 'tactics') diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e44d4cc7b..e1395ed8b 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -522,10 +522,13 @@ let respect_proj = lazy (mkConst (snd (List.hd (Lazy.force morphism_class).cl_pr let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let try_find_reference dir s = +let try_find_global_reference dir s = let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in - constr_of_global (Nametab.absolute_reference sp) - + Nametab.absolute_reference sp + +let try_find_reference dir s = + constr_of_global (try_find_global_reference dir s) + let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") @@ -537,13 +540,16 @@ let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") let coq_id = lazy (gen_constant ["Program"; "Basics"] "id") let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive") +let reflexive_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "reflexivity") let reflexive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "reflexivity") let symmetric_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Symmetric") let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "symmetry") +let symmetric_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "symmetry") let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive") let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity") +let transitive_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "transitivity") let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse" *) ["Program"; "Basics"] "flip") @@ -662,9 +668,9 @@ let find_class_proof proof_type proof_method env evars carrier relation = Typeclasses.resolve_one_typeclass env evars goal with e when Logic.catchable_exception e -> raise Not_found -let reflexive_proof env = find_class_proof reflexive_type reflexive_proof env -let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env -let transitive_proof env = find_class_proof transitive_type transitive_proof env +let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env +let get_symmetric_proof env = find_class_proof symmetric_type symmetric_proof env +let get_transitive_proof env = find_class_proof transitive_type transitive_proof env exception FoundInt of int @@ -831,7 +837,7 @@ let unify_eqn env sigma hypinfo t = let res = if l2r then (prf, (car, rel, c1, c2)) else - try (mkApp (symmetric_proof env Evd.empty car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1)) + try (mkApp (get_symmetric_proof env Evd.empty car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1)) with Not_found -> (prf, (car, inverse car rel, c2, c1)) in Some (env', res) @@ -1592,15 +1598,6 @@ let general_s_rewrite_clause x = let _ = Equality.register_general_setoid_rewrite_clause general_s_rewrite_clause -(* [setoid_]{reflexivity,symmetry,transitivity} tactics *) - -let relation_of_constr c = - match kind_of_term c with - | App (f, args) when Array.length args >= 2 -> - let relargs, args = array_chop (Array.length args - 2) args in - mkApp (f, relargs), args - | _ -> error "Not an applied relation." - let is_loaded d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in @@ -1610,36 +1607,139 @@ let try_loaded f gl = if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl else tclFAIL 0 (str"You need to require Coq.Classes.RelationClasses first") gl -let not_declared env ty car rel = - tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ - str ty ++ str" relation on carrier " ++ Printer.pr_constr_env env car) - -let setoid_proof gl ty fn = +let try_classes t gls = + try t gls + with (Pretype_errors.PretypeError _) as e -> raise e + +TACTIC EXTEND try_classes + [ "try_classes" tactic(t) ] -> [ try_classes (snd t) ] +END + +open Rawterm +open Environ +open Refiner + +let typeclass_app evm gl ?(bindings=NoBindings) c ty = + let nprod = nb_prod (pf_concl gl) in + let n = nb_prod ty - nprod in + if n<0 then error "Apply_tc: theorem has not enough premisses."; + Refiner.tclTHEN (Refiner.tclEVARS evm) + (fun gl -> + let clause = make_clenv_binding_apply gl (Some n) (c,ty) bindings in + let cl' = evar_clenv_unique_resolver true ~flags:default_unify_flags clause gl in + let evd' = Typeclasses.resolve_typeclasses cl'.env ~fail:true cl'.evd in + tclTHEN (Clenvtac.clenv_refine true {cl' with evd = evd'}) + tclNORMEVAR gl) gl + +open Tacinterp +open Pretyping + +let my_ist = + { lfun = []; + avoid_ids = []; + debug = Tactic_debug.DebugOff; + trace = [] } + +let rawconstr_and_expr (evd, c) = c + +let rawconstr_and_expr_of_rawconstr_bindings = function + | NoBindings -> NoBindings + | ImplicitBindings l -> ImplicitBindings (List.map rawconstr_and_expr l) + | ExplicitBindings l -> ExplicitBindings (List.map (fun (l,b,c) -> (l,b,rawconstr_and_expr c)) l) + +let my_glob_sign sigma env = { + ltacvars = [], [] ; + ltacrecvars = []; + gsigma = sigma ; + genv = env } + +let typeclass_app_constrexpr t ?(bindings=NoBindings) gl = let env = pf_env gl in - let rel, args = relation_of_constr (pf_concl gl) in -(* let evd, car = Evarutil.new_evar (create_evar_defs Evd.empty) env (new_Type ()) in -let evm = Evd.evars_of evd in*) - let evm, car = project gl, pf_type_of gl args.(0) in - try fn env evm car rel gl - with Not_found -> not_declared env ty car rel gl + let evars = ref (create_evar_defs (project gl)) in + let gs = my_glob_sign (project gl) env in + let t', bl = Tacinterp.intern_constr_with_bindings gs (t,bindings) in + let j = Pretyping.Default.understand_judgment_tcc evars env (fst t') in + let bindings = Tacinterp.interp_bindings my_ist gl bl in + typeclass_app (Evd.evars_of !evars) gl ~bindings:bindings j.uj_val j.uj_type +let typeclass_app_raw t gl = + let env = pf_env gl in + let evars = ref (create_evar_defs (project gl)) in + let j = Pretyping.Default.understand_judgment_tcc evars env t in + typeclass_app (Evd.evars_of !evars) gl j.uj_val j.uj_type + +let pr_gen prc _prlc _prtac c = prc c + +let pr_ceb _prc _prlc _prtac raw = mt () + +let interp_constr_expr_bindings _ _ t = t + +let intern_constr_expr_bindings ist t = t + +open Pcoq.Tactic + +type constr_expr_bindings = constr_expr with_bindings + +ARGUMENT EXTEND constr_expr_bindings + TYPED AS constr_expr_bindings + PRINTED BY pr_ceb + + INTERPRETED BY interp_constr_expr_bindings + GLOBALIZED BY intern_constr_expr_bindings + + + [ constr_with_bindings(c) ] -> [ c ] +END + +TACTIC EXTEND apply_typeclasses +[ "typeclass_app" constr_expr_bindings(t) ] -> [ typeclass_app_constrexpr (fst t) ~bindings:(snd t) ] +END +TACTIC EXTEND apply_typeclasses_abbrev +[ "tcapp" raw(t) ] -> [ typeclass_app_raw t ] +END + +(* [setoid_]{reflexivity,symmetry,transitivity} tactics *) + +let not_declared env ty rel = + tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ + str ty ++ str" relation. Maybe you need to import the Setoid library.") + +let relation_of_constr env c = + match kind_of_term c with + | App (f, args) when Array.length args >= 2 -> + let relargs, args = array_chop (Array.length args - 2) args in + mkApp (f, relargs), args + | _ -> errorlabstrm "relation_of_constr" + (str "The term " ++ Printer.pr_constr_env env c ++ str" is not an applied relation.") + +let setoid_proof gl ty ?(bindings=NoBindings) meth fallback = + try + typeclass_app_constrexpr + (CRef (Qualid (dummy_loc, Nametab.shortest_qualid_of_global Idset.empty + (Lazy.force meth)))) ~bindings gl + with Not_found | Typeclasses_errors.TypeClassError (_, _) | + Ploc.Exc (_, Typeclasses_errors.TypeClassError (_, _)) -> + match fallback gl with + | Some tac -> tac gl + | None -> + let env = pf_env gl in + let rel, args = relation_of_constr env (pf_concl gl) in + not_declared env ty rel gl + let setoid_reflexivity gl = - setoid_proof gl "reflexive" - (fun env evm car rel gl -> - apply (reflexive_proof env evm car rel) gl) - + setoid_proof gl "reflexive" reflexive_proof_global (reflexivity_red true) + let setoid_symmetry gl = - setoid_proof gl "symmetric" - (fun env evm car rel gl -> - apply (symmetric_proof env evm car rel) gl) - -let setoid_transitivity c gl = - setoid_proof gl "transitive" - (fun env evm car rel gl -> - apply_with_bindings - ((transitive_proof env evm car rel), - Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]) gl) + setoid_proof gl "symmetric" symmetric_proof_global (symmetry_red true) +let setoid_transitivity c gl = + let binding_name = + next_ident_away (id_of_string "y") (ids_of_named_context (named_context (pf_env gl))) + in + setoid_proof gl "transitive" + ~bindings:(Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp binding_name, constrIn c ]) + transitive_proof_global (transitivity_red true c) + let setoid_symmetry_in id gl = let ctype = pf_type_of gl (mkVar id) in let binders,concl = Sign.decompose_prod_assum ctype in @@ -1669,51 +1769,11 @@ TACTIC EXTEND setoid_symmetry END TACTIC EXTEND setoid_reflexivity - [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] +[ "setoid_reflexivity" ] -> [ setoid_reflexivity ] END TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] -END - -let try_classes t gls = - try t gls - with (Pretype_errors.PretypeError _) as e -> raise e - -TACTIC EXTEND try_classes - [ "try_classes" tactic(t) ] -> [ try_classes (snd t) ] -END - -open Rawterm - -let constrexpr = Pcoq.Tactic.open_constr -type 'a constr_expr_argtype = (open_constr_expr, 'a) Genarg.abstract_argument_type - -let (wit_constrexpr : Genarg.tlevel constr_expr_argtype), - (globwit_constrexpr : Genarg.glevel constr_expr_argtype), - (rawwit_const_expr : Genarg.rlevel constr_expr_argtype) = - Genarg.create_arg "constrexpr" - -open Environ -open Refiner - -let typeclass_app t gl = - let nprod = nb_prod (pf_concl gl) in - let env = pf_env gl in - let evars = ref (create_evar_defs (project gl)) in - let j = Pretyping.Default.understand_judgment_tcc evars env t in - let n = nb_prod j.uj_type - nprod in - if n<0 then error "Apply_tc: theorem has not enough premisses."; - Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !evars)) - (fun gl -> - let clause = make_clenv_binding_apply gl (Some n) (j.uj_val,j.uj_type) NoBindings in - let cl' = evar_clenv_unique_resolver true ~flags:default_unify_flags clause gl in - let evd' = Typeclasses.resolve_typeclasses cl'.env ~fail:true cl'.evd in - Clenvtac.clenv_refine true {cl' with evd = evd'} gl) gl - -TACTIC EXTEND apply_typeclasses - [ "typeclass_app" raw(t) ] -> [ typeclass_app t ] -(* | [ "app" raw(t) ] -> [ typeclass_app t ] *) +[ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] END let rec head_of_constr t = diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 98c0c1104..644a68666 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1942,82 +1942,82 @@ let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = (* [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let setoid_reflexivity gl = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_reflexivity" - [] (pf_concl gl) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_refl with - None -> - errorlabstrm "Setoid_reflexivity" - (str "The relation " ++ prrelation rel ++ str " is not reflexive.") - | Some refl -> apply refl gl - with - Optimize -> reflexivity_red true gl - -let setoid_symmetry gl = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_symmetry" - [] (pf_concl gl) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_sym with - None -> - errorlabstrm "Setoid_symmetry" - (str "The relation " ++ prrelation rel ++ str " is not symmetric.") - | Some sym -> apply sym gl - with - Optimize -> symmetry_red true gl - -let setoid_symmetry_in id gl = - let ctype = pf_type_of gl (mkVar id) in - let binders,concl = Sign.decompose_prod_assum ctype in - let (equiv, args) = decompose_app concl in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "The term provided is not an equivalence" - in - let others,(c1,c2) = split_last_two args in - let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in - let new_hyp' = mkApp (he, [| c2 ; c1 |]) in - let new_hyp = it_mkProd_or_LetIn new_hyp' binders in - tclTHENS (cut new_hyp) - [ intro_replacing id; - tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ] - gl - -let setoid_transitivity c gl = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_transitivity" - [] (pf_concl gl) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - let ctyp = pf_type_of gl c in - let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in - match rel'.rel_trans with - None -> - errorlabstrm "Setoid_transitivity" - (str "The relation " ++ prrelation rel ++ str " is not transitive.") - | Some trans -> - let transty = nf_betaiota (pf_type_of gl trans) in - let argsrev, _ = - Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in - let binder = - match List.rev argsrev with - _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2 - | _ -> assert false - in - apply_with_bindings - (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl - with - Optimize -> transitivity_red true c gl -;; +(* let setoid_reflexivity gl = *) +(* try *) +(* let relation_class = *) +(* relation_class_that_matches_a_constr "Setoid_reflexivity" *) +(* [] (pf_concl gl) in *) +(* match relation_class with *) +(* Leibniz _ -> assert false (\* since [] is empty *\) *) +(* | Relation rel -> *) +(* match rel.rel_refl with *) +(* None -> *) +(* errorlabstrm "Setoid_reflexivity" *) +(* (str "The relation " ++ prrelation rel ++ str " is not reflexive.") *) +(* | Some refl -> apply refl gl *) +(* with *) +(* Optimize -> reflexivity_red true gl gl *) + +(* let setoid_symmetry gl = *) +(* try *) +(* let relation_class = *) +(* relation_class_that_matches_a_constr "Setoid_symmetry" *) +(* [] (pf_concl gl) in *) +(* match relation_class with *) +(* Leibniz _ -> assert false (\* since [] is empty *\) *) +(* | Relation rel -> *) +(* match rel.rel_sym with *) +(* None -> *) +(* errorlabstrm "Setoid_symmetry" *) +(* (str "The relation " ++ prrelation rel ++ str " is not symmetric.") *) +(* | Some sym -> apply sym gl *) +(* with *) +(* Optimize -> symmetry_red true gl *) + +(* let setoid_symmetry_in id gl = *) +(* let ctype = pf_type_of gl (mkVar id) in *) +(* let binders,concl = Sign.decompose_prod_assum ctype in *) +(* let (equiv, args) = decompose_app concl in *) +(* let rec split_last_two = function *) +(* | [c1;c2] -> [],(c1, c2) *) +(* | x::y::z -> let l,res = split_last_two (y::z) in x::l, res *) +(* | _ -> error "The term provided is not an equivalence" *) +(* in *) +(* let others,(c1,c2) = split_last_two args in *) +(* let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in *) +(* let new_hyp' = mkApp (he, [| c2 ; c1 |]) in *) +(* let new_hyp = it_mkProd_or_LetIn new_hyp' binders in *) +(* tclTHENS (cut new_hyp) *) +(* [ intro_replacing id; *) +(* tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ] *) +(* gl *) + +(* let setoid_transitivity c gl = *) +(* try *) +(* let relation_class = *) +(* relation_class_that_matches_a_constr "Setoid_transitivity" *) +(* [] (pf_concl gl) in *) +(* match relation_class with *) +(* Leibniz _ -> assert false (\* since [] is empty *\) *) +(* | Relation rel -> *) +(* let ctyp = pf_type_of gl c in *) +(* let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in *) +(* match rel'.rel_trans with *) +(* None -> *) +(* errorlabstrm "Setoid_transitivity" *) +(* (str "The relation " ++ prrelation rel ++ str " is not transitive.") *) +(* | Some trans -> *) +(* let transty = nf_betaiota (pf_type_of gl trans) in *) +(* let argsrev, _ = *) +(* Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in *) +(* let binder = *) +(* match List.rev argsrev with *) +(* _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2 *) +(* | _ -> assert false *) +(* in *) +(* apply_with_bindings *) +(* (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl *) +(* with *) +(* Optimize -> transitivity_red true c gl *) +(* ;; *) diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 244e02dd4..e1ab9255d 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -64,10 +64,10 @@ val general_s_rewrite : val general_s_rewrite_in : identifier -> bool -> occurrences -> constr -> new_goals:constr list -> tactic -val setoid_reflexivity : tactic -val setoid_symmetry : tactic -val setoid_symmetry_in : identifier -> tactic -val setoid_transitivity : constr -> tactic +(* val setoid_reflexivity : tactic *) +(* val setoid_symmetry : tactic *) +(* val setoid_symmetry_in : identifier -> tactic *) +(* val setoid_transitivity : constr -> tactic *) val add_relation : Names.identifier -> constr_expr -> constr_expr -> constr_expr option -> diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 5c040821b..0d41db8a4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -99,6 +99,10 @@ val intern_tactic : val intern_constr : glob_sign -> constr_expr -> rawconstr_and_expr +val intern_constr_with_bindings : + glob_sign -> constr_expr * constr_expr Rawterm.bindings -> + rawconstr_and_expr * rawconstr_and_expr Rawterm.bindings + val intern_hyp : glob_sign -> identifier Util.located -> identifier Util.located @@ -124,6 +128,9 @@ val interp_tac_gen : (identifier * value) list -> identifier list -> val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier +val interp_bindings : interp_sign -> goal sigma -> rawconstr_and_expr Rawterm.bindings -> + Evd.open_constr Rawterm.bindings + (* Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr diff --git a/tactics/tactics.ml b/tactics/tactics.ml index afc4a9b96..ac7691282 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2794,12 +2794,15 @@ let reflexivity_red allowred gl = let concl = if not allowred then pf_concl gl else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) in - match match_with_equation concl with - | None -> !setoid_reflexivity gl - | Some _ -> one_constructor 1 NoBindings gl - -let reflexivity gl = reflexivity_red false gl - + match match_with_equation concl with + | None -> None + | Some _ -> Some (one_constructor 1 NoBindings) + +let reflexivity gl = + match reflexivity_red false gl with + | None -> !setoid_reflexivity gl + | Some tac -> tac gl + let intros_reflexivity = (tclTHEN intros reflexivity) (* Symmetry tactics *) @@ -2819,9 +2822,9 @@ let symmetry_red allowred gl = let concl = if not allowred then pf_concl gl else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) in - match match_with_equation concl with - | None -> !setoid_symmetry gl - | Some (hdcncl,args) -> + match match_with_equation concl with + | None -> None + | Some (hdcncl,args) -> Some (fun gl -> let hdcncls = string_of_inductive hdcncl in begin try @@ -2839,9 +2842,12 @@ let symmetry_red allowred gl = tclLAST_HYP simplest_case; one_constructor 1 NoBindings ]) gl - end + end) -let symmetry gl = symmetry_red false gl +let symmetry gl = + match symmetry_red false gl with + | None -> !setoid_symmetry gl + | Some tac -> tac gl let setoid_symmetry_in = ref (fun _ _ -> assert false) let register_setoid_symmetry_in f = setoid_symmetry_in := f @@ -2891,8 +2897,8 @@ let transitivity_red allowred t gl = else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) in match match_with_equation concl with - | None -> !setoid_transitivity t gl - | Some (hdcncl,args) -> + | None -> None + | Some (hdcncl,args) -> Some (fun gl -> let hdcncls = string_of_inductive hdcncl in begin try @@ -2916,10 +2922,13 @@ let transitivity_red allowred t gl = [ tclDO 2 intro; tclLAST_HYP simplest_case; assumption ])) gl - end - -let transitivity t gl = transitivity_red false t gl + end) +let transitivity t gl = + match transitivity_red false t gl with + | None -> !setoid_transitivity t gl + | Some tac -> tac gl + let intros_transitivity n = tclTHEN intros (transitivity n) (* tactical to save as name a subproof such that the generalisation of diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 56597f58e..d3d353f17 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -324,19 +324,19 @@ val simplest_split : tactic (*s Logical connective tactics. *) val register_setoid_reflexivity : tactic -> unit -val reflexivity_red : bool -> tactic +val reflexivity_red : bool -> goal sigma -> tactic option val reflexivity : tactic val intros_reflexivity : tactic val register_setoid_symmetry : tactic -> unit -val symmetry_red : bool -> tactic +val symmetry_red : bool -> goal sigma -> tactic option val symmetry : tactic val register_setoid_symmetry_in : (identifier -> tactic) -> unit val symmetry_in : identifier -> tactic val intros_symmetry : clause -> tactic val register_setoid_transitivity : (constr -> tactic) -> unit -val transitivity_red : bool -> constr -> tactic +val transitivity_red : bool -> constr -> goal sigma -> tactic option val transitivity : constr -> tactic val intros_transitivity : constr -> tactic -- cgit v1.2.3