(* Coq keywords, depending on version.
   Copyright (C) 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "coq_kw_h";

fun coq_keywords "7" =
    |[forall_prolog = "(",
      forall_midlog = ")",
      fun_paren_prolog = "[",
      fun_prolog = "[",
      fun_midlog = "]",
      fun_paren_epilog = "",
      exists_prolog = "(EX ",
      exists_midlog = " | ",
      exists_epilog = ")",
      case_prolog = "Cases ",
      case_delim = " ",
      case_of = " of",
      case_midlog = " => ",
      case_epilog = "end",
      param_prolog = "[",
      param_delim = "; ",
      param_epilog = "]",
      var_delim = ", ",
      rec_def = "Fixpoint ",
      plain_def = "Fixpoint ",
      dot_tac = ".",
      semi_tac = "; ",
      clear_tac = "Clear ",
      intros_tac = "Intros",
      intro_tac = "Intro ",
      tauto_tac = "Tauto",
      exact_tac = "Exact ",
      trivial_tac = "Trivial",
      unfold_tac = "Unfold ",
      exists_tac = "Exists ",
      inversion_tac = "Inversion ",
      destruct_tac = "Destruct ",
      intuition_tac = "Intuition ",
      auto_tac = "Auto ",
      apply_tac = "Apply ",
      eapply_tac = "EApply ",
      refl_tac = "Reflexivity",
      assum_tac = "Assumption",
      left_tac = "Left",
      right_tac = "Right",
      cut_tac = "Cut ",
      cut_end = "",
      elim_tac = "Elim ",
      induction_tac = "Induction ",
      case_tac = "Case ",
      fix_tac = "Fix ",
      first_tac = "First ",
      split_tac = "Split",
      simpl_tac = "Simpl",
      try_tac = "Try ",
      rewrite_tac = "Rewrite ",
      assert_tac = "Assert ", (* I don't know whether that really existed in v7. *)
      discr_tac = "Discriminate",
      decomp_sum_tac = "Decompose Sum", (* I don't know whether that really existed in v7. *)
      refine_tac = "Refine "
      ]|
  | coq_keywords _ =
    |[forall_prolog = "forall ",
      forall_midlog = ", ",
      fun_paren_prolog = "(fun ",
      fun_prolog = "fun ",
      fun_midlog = " => ",
      fun_paren_epilog = ")",
      exists_prolog = "exists ",
      exists_midlog = ", ",
      exists_epilog = "",
      case_prolog = "match ",
      case_delim = ",",
      case_of = " with",
      case_midlog = " => ",
      case_epilog = "end",
      param_prolog = "(",
      param_delim = ") (",
      param_epilog = ")",
      var_delim = " ",
      rec_def = "Fixpoint ",
      plain_def = "Definition ",
      dot_tac = ".",
      semi_tac = "; ",
      clear_tac = "clear ",
      intros_tac = "intros",
      intro_tac = "intro ",
      tauto_tac = "tauto",
      exact_tac = "exact ",
      trivial_tac = "trivial",
      unfold_tac = "unfold ",
      exists_tac = "exists ",
      inversion_tac = "inversion ",
      destruct_tac = "destruct ",
      intuition_tac = "intuition ",
      auto_tac = "auto ",
      apply_tac = "apply ",
      eapply_tac = "eapply ",
      refl_tac = "reflexivity",
      assum_tac = "assumption",
      left_tac = "left",
      right_tac = "right",
      cut_tac = "cut (",
      cut_end = ")",
      elim_tac = "elim ",
      induction_tac = "induction ",
      case_tac = "case ",
      fix_tac = "fix ",
      first_tac = "first ",
      split_tac = "split",
      simpl_tac = "simpl",
      try_tac = "try ",
      rewrite_tac = "rewrite ",
      assert_tac = "assert ",
      discr_tac = "discriminate",
      decomp_sum_tac = "decompose sum",
      refine_tac = "refine "
      ]|;
