diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 8 | ||||
| -rw-r--r-- | plugins/ring/ring.ml | 4 |
3 files changed, 7 insertions, 7 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bba3f95fd5..1d1e4a2a68 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1416,7 +1416,7 @@ let rec rewrite_eqs_in_eqs eqs = (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) - (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* dep proofs also: *) true id (mkVar eq) false)) + (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* dep proofs also: *) true id (mkVar eq) false)) gl ) eqs diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5b689625bc..9b1ccde2c1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -373,7 +373,7 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool) h_intros thin_intros; tclMAP - (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* deps proofs also: *) true teq eq false)) + (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* deps proofs also: *) true teq eq false)) (List.rev eqs); (fun g1 -> let ty_teq = pf_type_of g1 (mkVar teq) in @@ -534,7 +534,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = in tclTHENS (general_rewrite_bindings false Termops.all_occurrences - (* dep proofs also: *) true + (* dep proofs also: *) true true (mkVar eq, ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; dummy_loc, NamedHyp def_id, mkVar def]) false) @@ -1211,7 +1211,7 @@ let rec introduce_all_values_eq cont_tac functional termine Nameops.out_name def_na in observe_tac "rewrite heq" (general_rewrite_bindings false Termops.all_occurrences - (* dep proofs also: *) true (mkVar heq2, + true (* dep proofs also: *) true (mkVar heq2, ExplicitBindings[dummy_loc,NamedHyp def_id, f]) false) gls) [tclTHENLIST @@ -1266,7 +1266,7 @@ let rec introduce_all_values_eq cont_tac functional termine f_S(mkVar pmax'); dummy_loc, NamedHyp def_id, f]) in - observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences (* dep proofs also: *) true + observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences true (* dep proofs also: *) true c_b false)) g ) diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 7588e6a2fa..89309e3232 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -820,9 +820,9 @@ let raw_polynom th op lc gl = (tclTHENS (tclORELSE (Equality.general_rewrite true - Termops.all_occurrences false c'i_eq_c''i) + Termops.all_occurrences true false c'i_eq_c''i) (Equality.general_rewrite false - Termops.all_occurrences false c'i_eq_c''i)) + Termops.all_occurrences true false c'i_eq_c''i)) [tac])) else (tclORELSE |