From f4cdaa1a48ac6f4fbef567b8a8ddf3fcfc97a3cd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 May 2006 13:41:52 +0000 Subject: [PATCH] Bug fixed in fresh_name_generator: the function used to fail on beta redexes. Fixed trivially without introducing yet another whd. --- .../components/cic_proof_checking/freshNamesGenerator.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml index 5f3bfdbbd..1edb35b04 100755 --- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml +++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml @@ -60,7 +60,9 @@ let rec guess_a_name context ty = | Cic.Implicit _ -> assert false | Cic.Cast (t1,t2) -> guess_a_name context t1 | Cic.Prod (na_,_,t) -> higher_name 1 t - | Cic.Lambda _ -> assert false +(* warning: on appl we should beta reduce before the recursive call + | Cic.Lambda _ -> assert false +*) | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t) | Cic.Appl [] -> assert false | Cic.Appl (he::_) -> guess_a_name context he -- 2.39.2