let rec aux context term =
match (context, term) with
| Cic.Implicit (Some `Hole), t -> [t]
+ | Cic.Implicit None,_ -> []
| Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
List.concat
(List.map2
| Cic.CurrentProof (_, _, _, _, _, attributes)
| Cic.InductiveDefinition (_, _, _, attributes) ->
attributes
+
+let rec mk_rels howmany from =
+ match howmany with
+ | 0 -> []
+ | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)