| 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"
with CicTypeChecker.TypeCheckerFailure _ -> "H"
)
| C.Name name ->
- Str.global_replace (Str.regexp "[0-9]*$") "" name
+ Str.global_replace (Str.regexp "[0-9']*$") "" name
in
let already_used name =
List.exists (function Some (n,_) -> n=name | _ -> false) context