The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I am trying to create a tactic "arewrite" that will change the conclusion of a goal.

For example, if I have the state:

  a, b, c : nat

  ============================

  eval (c :: (b :: a :: nil)%list)

    (a_plus (a_plus (a_var 1) (a_var 0)) (a_const 1)) <=

  eval (c :: (b :: a :: nil)%list) (a_var 2)

Apply "arewrite" should yield the state:

  a, b, c : nat

  ============================

  2=3

I am trying to do this with the code below.

let test_eq = lazy (Lib_coq.init_constant ["Coq";"Init";"Logic"] "eq")

let test_term = Term.mkApp (Lazy.force test_eq, [|Lib_coq.Nat.of_int 2;Lib_coq.Nat.of_int 3|])

(* Top-level arewrite functionality *)

let arewrite : unit Proofview.tactic =

  Proofview.Goal.enter (fun gl ->

  let concl = Proofview.Goal.raw_concl gl in

  let (evm, env) = Lemmas.get_current_context() in

  (*let (body, _) = Constrintern.interp_constr env evm concl in*)

  let _ = print "******* BEGIN *******" in

  let ast = apply_to_definition build_ast env 0 test_term in

  let _ = print ast in

  let _ = print "******* MIDDLE *******" in

  let ast = apply_to_definition build_ast env 0 concl in

  let _ = print ast in

  let _ = print "******* END *******" in

  (print_string "This is a test";

   (*Tacticals.New.tclFAIL 1

    (Pp.str "The tactic is not imlplemented.")*)

          Tacticals.New.tclTHENLIST

            [

              (** Our list of tactics consists in the following single

                  tactic, that changes the conclusion of the goal to

                  [concl'] if [concl] and [concl'] are convertible.

                  (see [tactics/tactis.mli] for other tactics.)  *)

              Tactics.change_concl test_term ;

            ]))

end

However, when I apply the tactic, I get "Error: Not a type.".  What do I need to change?

                          - Ken