| 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
- | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst s t)
+(* 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
| Cic.Const (uri,_)
(try
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context typ
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph
+ in
(match ty with
C.Sort C.Prop
| C.Sort C.CProp -> "H"