From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 Nov 2005 18:38:28 +0000 (+0000)
Subject: Comments changed/removed.
X-Git-Tag: V_0_7_2_3~45
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4a76b661a1130ce6afcfde9305579682b5458106

Comments changed/removed.
---

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index e519827f2..b603bff9e 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -33,7 +33,6 @@ let rec rewrite_tac ~direction ~pattern equality =
   let module PEH = ProofEngineHelpers in
   let module PT = PrimitiveTactics in
   assert (wanted = None);   (* this should be checked syntactically *)
-  (*assert (hyps_pat = []); (*CSC: not implemented yet! *)*)
   let proof,goal = status in
   let curi, metasenv, pbo, pty = proof in
   let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
@@ -57,13 +56,12 @@ let rec rewrite_tac ~direction ~pattern equality =
    match hyps_pat with
       [] -> None,true,PT.exact_tac,concl_pat,gty
     | [name,pat] ->
-      (*CSC: bug here; I am ignoring the concl_pat *)
       let rec find_hyp n =
        function
           [] -> assert false
         | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
            Cic.Rel n, CicSubstitution.lift n ty
-        | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet!*)
+        | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet! But does this make any sense?*)
         | _::tl -> find_hyp (n+1) tl
       in
        let arg,gty = find_hyp 1 context in