From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Mar 2006 12:13:16 +0000 (+0000)
Subject: reverted the addition of _ to mistyped names
X-Git-Tag: make_still_working~7450
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0242faad2b940b1cf5961ea9241854b31866fd65;p=helm.git

reverted the addition of _ to mistyped names
---

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 32daa4945..2a7a3f2d0 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -79,10 +79,10 @@ let rec pp t l =
     | C.Var (uri,exp_named_subst) ->
        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
-       "?" ^ (string_of_int n) (* ^ "[" ^ 
+       "?" ^ (string_of_int n) ^ "[" ^ 
         String.concat " ; "
          (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-        "]" *)
+        "]"
     | C.Sort s ->
        (match s with
            C.Prop  -> "Prop"
@@ -357,7 +357,7 @@ let rec check_rec ctx string_name =
     | Cic.Implicit _ -> string_name
     | Cic.Cast (te,ty) -> check_rec ctx string_name te
     | Cic.Prod (name,so,dest) -> 
-	let _l_string_name = check_rec ctx string_name so in
+	let l_string_name = check_rec ctx string_name so in
 	check_rec (name::ctx) string_name dest
     | Cic.Lambda (name,so,dest) -> 
         let string_name =
@@ -390,11 +390,11 @@ let rec check_rec ctx string_name =
 	  | _ -> assert false) in
 	remove_prefix name string_name  
     | Cic.MutCase (_,_,_,te,pl) ->
-	let _strig_name = remove_prefix "match" string_name in
+	let strig_name = remove_prefix "match" string_name in
 	let string_name = check_rec ctx string_name te in
         List.fold_right (fun t s -> check_rec ctx s t) pl string_name
     | Cic.Fix (_,fl) ->
-        let _strig_name = remove_prefix "fix" string_name in
+        let strig_name = remove_prefix "fix" string_name in
         let names = List.map (fun (name,_,_,_) -> name) fl in
         let onames =
           List.rev (List.map (function name -> Cic.Name name) names)
@@ -402,7 +402,7 @@ let rec check_rec ctx string_name =
         List.fold_right 
 	  (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
     | Cic.CoFix (_,fl) ->
-	let _strig_name = remove_prefix "cofix" string_name in
+	let strig_name = remove_prefix "cofix" string_name in
         let names = List.map (fun (name,_,_) -> name) fl in
         let onames =
           List.rev (List.map (function name -> Cic.Name name) names)