-let annotate_term ann term =
- let module C = Cic in
- let rann =
- match term with
- C.ARel (_, rann, _, _) -> rann
- | C.AVar (_, rann, _) -> rann
- | C.AMeta (_, rann, _) -> rann
- | C.ASort (_, rann, _) -> rann
- | C.AImplicit (_, rann) -> rann
- | C.ACast (_, rann, _, _) -> rann
- | C.AProd (_, rann, _, _, _) -> rann
- | C.ALambda (_, rann, _, _, _) -> rann
- | C.ALetIn (_, rann, _, _, _) -> rann
- | C.AAppl (_, rann, _) -> rann
- | C.AConst (_, rann, _, _) -> rann
- | C.AAbst (_, rann, _) -> rann
- | C.AMutInd (_, rann, _, _, _) -> rann
- | C.AMutConstruct (_, rann, _, _, _, _) -> rann
- | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann
- | C.AFix (_, rann, _, _) -> rann
- | C.ACoFix (_, rann, _, _) -> rann
- in
- rann := Some ann