diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 8 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 3 |
4 files changed, 4 insertions, 11 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 66c72a30a2..4f20e5a800 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -43,7 +43,7 @@ DECLARE PLUGIN "ltac_plugin" (**********************************************************************) (* replace, discriminate, injection, simplify_eq *) -(* cutrewrite, dependent rewrite *) +(* dependent rewrite *) let with_delayed_uconstr ist c tac = let flags = { @@ -203,12 +203,6 @@ TACTIC EXTEND dependent_rewrite -> { rewriteInHyp b c id } END -TACTIC EXTEND cut_rewrite -| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } -| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] - -> { cutRewriteInHyp b eqn id } -END - (**********************************************************************) (* Decompose *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6233807016..f69fe064a7 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s = ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) | TacChange (check,op,c,h) -> - let name = if check then "change_no_check" else "change" in + let name = if check then "change" else "change_no_check" in hov 1 ( primitive name ++ brk (1,1) ++ ( diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fb149071c9..a1dbf9a439 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.allowed_evars = Unification.AllowAll; + Unification.allowed_evars = Evarsolve.AllowedEvars.all; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 2ca9a0e69d..88480194c8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2125,8 +2125,7 @@ let _ = (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) - let name, poly = Id.of_string "ltac_gen", poly in - let name, poly = Id.of_string "ltac_gen", poly in + let name = Id.of_string "ltac_gen" in let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in |