From 4a76b661a1130ce6afcfde9305579682b5458106 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 17 Nov 2005 18:38:28 +0000 Subject: [PATCH] Comments changed/removed. --- helm/ocaml/tactics/equalityTactics.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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 -- 2.39.2