Comments changed/removed.

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index e519827f22918328784e7e15a4a6b97a515d6546..b603bff9ed31b1cb48a6cbc54bae221ef0816333 100644 (file)
--- 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