| l -> idref aid (Ast.Appl l)
in
let deannot_he = Deannotate.deannotate_term he in
- if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions
+ if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions
then
- match CoercGraph.is_a_coercion_to_funclass deannot_he with
+ match CoercDb.is_a_coercion_to_funclass deannot_he with
| None -> idref aid (last_n 1 (List.map k tl))
| Some i -> idref aid (last_n (i+1) (List.map k tl))
else
let defs =
List.map
(fun (_, n, decr_idx, ty, bo) ->
- ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
+ let params,bo =
+ let rec aux =
+ function
+ Cic.ALambda (_,name,so,ta) ->
+ let params,rest = aux ta in
+ (CicNotationUtil.name_of_cic_name name,Some (k so))::
+ params, rest
+ | t -> [],t
+ in
+ aux bo
+ in
+ let ty =
+ let rec eat_pis =
+ function
+ 0,ty -> ty
+ | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+ | n,ty ->
+ (* I should do a whd here, but I have no context *)
+ assert false
+ in
+ eat_pis ((List.length params),ty)
+ in
+ (params,(Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
funs
in
let name =
try
(match List.nth defs no with
- | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+ | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
| _ -> assert false)
with Not_found -> assert false
in
- idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
+ idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
| Cic.ACoFix (id, no, funs) ->
let defs =
List.map
(fun (_, n, ty, bo) ->
- ((Ast.Ident (n, None), Some (k ty)), k bo, 0))
+ let params,bo =
+ let rec aux =
+ function
+ Cic.ALambda (_,name,so,ta) ->
+ let params,rest = aux ta in
+ (CicNotationUtil.name_of_cic_name name,Some (k so))::
+ params, rest
+ | t -> [],t
+ in
+ aux bo
+ in
+ let ty =
+ let rec eat_pis =
+ function
+ 0,ty -> ty
+ | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+ | n,ty ->
+ (* I should do a whd here, but I have no context *)
+ assert false
+ in
+ eat_pis ((List.length params),ty)
+ in
+ (params,(Ast.Ident (n, None), Some (k ty)), k bo, 0))
funs
in
let name =
try
(match List.nth defs no with
- | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+ | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
| _ -> assert false)
with Not_found -> assert false
in