-let rec lookup_tactic = function
- | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
- | TacticAst.Intros (_, names) ->
- let namer =
- (** use names given by the user as long as they are availble, then
- * fallback on default fresh name generator *)
- let len = List.length names in
- let count = ref 0 in
- fun metasenv context name ~typ ->
- if !count < len then begin
- let name = Cic.Name (List.nth names !count) in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
- in
- PrimitiveTactics.intros_tac ~mk_fresh_name_callback:namer ()
- | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
- | TacticAst.Assumption -> VariousTactics.assumption_tac
- | TacticAst.Contradiction -> NegationTactics.contradiction_tac
- | TacticAst.Exists -> IntroductionTactics.exists_tac
- | TacticAst.Fourier -> FourierR.fourier_tac
- | TacticAst.Left -> IntroductionTactics.left_tac
- | TacticAst.Right -> IntroductionTactics.right_tac
- | TacticAst.Ring -> Ring.ring_tac
- | TacticAst.Split -> IntroductionTactics.split_tac
- | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
-(*
- (* TODO Zack a lot more of tactics to be implemented here ... *)
- | TacticAst.Absurd
- | TacticAst.Apply of 'term
- | TacticAst.Change of 'term * 'term * 'ident option
- | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
- | TacticAst.Cut of 'term
- | TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Discriminate of 'ident
- | TacticAst.Elim of 'term * 'term option
- | TacticAst.ElimType of 'term
- | TacticAst.Exact of 'term
- | TacticAst.Fold of reduction_kind * 'term
- | TacticAst.Injection of 'ident
- | TacticAst.Intros of int option * 'ident list
- | TacticAst.LetIn of 'term * 'ident
- | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
- | TacticAst.Replace of 'term * 'term
- | TacticAst.Replace_pattern of 'term pattern * 'term
- | TacticAst.Rewrite of direction * 'term * 'ident option
- | TacticAst.Transitivity of 'term
-*)
- | _ ->
- MatitaTypes.not_implemented "some tactic"
+ (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+ * names as long as they are available, then it fallbacks to name generation
+ * using FreshNamesGenerator module *)
+let namer_of names =
+ let len = List.length names in
+ let count = ref 0 in
+ fun metasenv context name ~typ ->
+ if !count < len then begin
+ let name = Cic.Name (List.nth names !count) in
+ incr count;
+ name
+ end else
+ FreshNamesGenerator.mk_fresh_name metasenv context name ~typ