From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 7 Jul 2005 14:48:41 +0000 (+0000)
Subject: Names bound in lambdas can now be used in the "canonical" name of the theorem.
X-Git-Tag: V_0_7_1~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec9a40eb3f7c777f20ae179d083265f22cd5e858;p=helm.git

Names bound in lambdas can now be used in the "canonical" name of the theorem.
---

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 7a1de4a7f..effc8a4b5 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -311,6 +311,10 @@ let check_name ctx name term =
 	  let string_name = check_aux ctx string_name so in
 	  check_aux (name::ctx) string_name dest
       | Cic.Lambda (name,so,dest) -> 
+          let string_name =
+           match name with
+              Cic.Anonymous -> string_name
+            | Cic.Name name -> cut_off_name name string_name in
           let string_name = check_aux ctx string_name so in
 	  check_aux (name::ctx) string_name dest
       | Cic.LetIn (name,so,dest) ->