From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 26 Sep 2005 09:35:42 +0000 (+0000)
Subject: Small bug due to case unsensitiveness in the check function.
X-Git-Tag: LAST_BEFORE_NEW~8
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15e1fe3260e890b9a206b898084e8f19253a13b7;p=helm.git

Small bug due to case unsensitiveness in the check function.
---

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