if localize then
match body with
CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
- let l' = List.map (aux ~localize loc context') l in
+ (* since we avoid the letin, the context has no
+ * recfuns in it *)
+ let l' = List.map (aux ~localize loc context) l in
`AvoidLetIn (n,l')
| _ -> assert false
else
| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
- | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+ | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)