+let assumption status goal =
+ let gty = get_goalty status goal in
+ let context = ctx_of gty in
+ let (htac:NTacStatus.tactic) =
+ first_tac (List.map
+ (fun (name,_) ->
+ exact_tac ("",0,(Ast.Ident (name,None))))
+ context)
+ in
+ exec htac status goal
+;;
+
+let assumption_tac =
+ distribute_tac assumption
+;;
+