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 7a1de4a7fd06919c7771386bd6f74942fad45225..effc8a4b58b7450bf71100ea62dc8fc1d97f7610 100644 (file)
--- 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) ->