diff options
| author | herbelin | 2004-07-16 20:14:12 +0000 |
|---|---|---|
| committer | herbelin | 2004-07-16 20:14:12 +0000 |
| commit | cbb8368f2345d2f2d779ca35bc634e49e3d50e3b (patch) | |
| tree | f77608eac40fd2afcd0ad0d53414ccc488f8a7cd /parsing/g_tactic.ml4 | |
| parent | 763cf4f37e10d9a0e8a2a0e9286c02708a60bf08 (diff) | |
Suppression quotify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5922 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 3d1d8eea65..7c4fa0d5bc 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -15,10 +15,6 @@ open Util open Tacexpr open Rawterm open Genarg - -(* open grammar entries, possibly in quotified form *) -ifdef Quotify then open Qast - open Constr open Prim open Tactic @@ -39,24 +35,6 @@ let local_compute = [FBeta;FIota;FDeltaBut [];FZeta] let error_oldelim _ = error "OldElim no longer supported" -ifdef Quotify then - let induction_arg_of_constr = function - | Qast.Node ("Nvar", [_;id]) -> Qast.Node ("ElimOnIdent", [id]) - | c -> Qast.Node ("ElimOnConstr", [c]) - -ifdef Quotify then -let make_red_flag s = Qast.Apply ("make_red_flag", [s]) - -ifdef Quotify then -let local_compute = - Qast.List [ - Qast.Node ("FBeta", []); - Qast.Node ("FDeltaBut", [Qast.List []]); - Qast.Node ("FIota", []); - Qast.Node ("FZeta", [])] - -ifdef Quotify then open Q - let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) (* Auxiliary grammar rules *) |