From 15e1fe3260e890b9a206b898084e8f19253a13b7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 26 Sep 2005 09:35:42 +0000 Subject: [PATCH] Small bug due to case unsensitiveness in the check function. --- helm/ocaml/cic_proof_checking/cicPp.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 93d7d0a04..9242d1fed 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -295,8 +295,8 @@ let is_prefix prefix string = if len <= len1 then begin let head = String.sub string 0 len in - if ((String.compare head prefix)=0) || - ((String.compare head (String.lowercase prefix))=0) then + if + (String.compare (String.lowercase head) (String.lowercase prefix)=0) then begin let diff = len1-len in let tail = String.sub string len diff in @@ -309,6 +309,11 @@ let is_prefix prefix string = else None let remove_prefix prefix (last,string) = + if prefix="append" then + begin + prerr_endline last; + prerr_endline string; + end; if string = "" then (last,string) else match is_prefix prefix string with @@ -452,6 +457,8 @@ let rec check_names ctx hyp_names conclusion_name t = hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t let check name term = +(* prerr_endline name; + prerr_endline (ppterm term); *) let names = Str.split (Str.regexp_string "_to_") name in let hyp_names,conclusion_name = match List.rev names with -- 2.39.2