1. "by proof" now allowed as a justification in equality chains.

[helm.git] / helm / software / components / tactics / declarative.ml

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 24801542dabcb76f57a6684a6d60fccaef31a488..b0615edb36c728415c5a03e8926278f03c3006a3 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -193,6 +193,8 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
               ~universe:(Universe.index Universe.empty 
                  (Universe.key ty) just) ~steps:1 ()
          (* Tactics.apply just *)
+    | `Proof ->
+        Tacticals.id_tac
   in
    let plhs,prhs,prepare =
     match lhs with