type goal = int
type status = proof * goal
+let initial_status ty metasenv =
+ let rec aux max = function
+ | [] -> max + 1
+ | (idx, _, _) :: tl ->
+ if idx > max then
+ aux idx tl
+ else
+ aux max tl
+ in
+ let newmeta_idx = aux 0 metasenv in
+ let proof =
+ None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty
+ in
+ (proof, newmeta_idx)
+
(**
a tactic: make a transition from one status to another one or, usually,
raise a "Fail" (@see Fail) exception in case of failure
(** creates an opaque tactic from a status->proof*goal list function *)
let mk_tactic t = t
+ (** what, hypothesis patterns, conclusion pattern *)
+type pattern = Cic.term option * (string * Cic.term) list * Cic.term
+let conclusion_pattern t = t,[],Cic.Implicit (Some `Hole)
+
(** tactic failure *)
exception Fail of string
universe graph if the tactic Fails
*)
let apply_tactic t status =
- let saved_univ = CicUniv.get_working() in
- try
- t status
- with Fail s -> CicUniv.set_working saved_univ; raise (Fail s)
+ t status
(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =