From ec9a40eb3f7c777f20ae179d083265f22cd5e858 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Jul 2005 14:48:41 +0000 Subject: [PATCH] Names bound in lambdas can now be used in the "canonical" name of the theorem. --- helm/ocaml/cic_proof_checking/cicPp.ml | 4 ++++ 1 file changed, 4 insertions(+) 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) -> -- 2.39.2