diff options
| author | Pierre-Marie Pédrot | 2016-04-14 20:43:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-04 13:47:12 +0200 |
| commit | a2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 (patch) | |
| tree | 88108ed4457cb0b573e468752619a2939085dd1a /ltac | |
| parent | de4b9b68445d9f3e48da789404cbdfcd89214585 (diff) | |
More toplevel value representation sharing.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index eda530c265..925c1679f2 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -938,12 +938,6 @@ type cmp = type 'i test = | Test of cmp * 'i * 'i -let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp" -let _ = Geninterp.register_val0 wit_cmp None -let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = - Genarg.make0 "tactest" -let _ = Geninterp.register_val0 wit_test None - let pr_cmp = function | Eq -> Pp.str"=" | Lt -> Pp.str"<" @@ -966,7 +960,7 @@ let pr_itest' _prc _prlc _prt = pr_itest -ARGUMENT EXTEND comparison TYPED AS cmp PRINTED BY pr_cmp' +ARGUMENT EXTEND comparison PRINTED BY pr_cmp' | [ "=" ] -> [ Eq ] | [ "<" ] -> [ Lt ] | [ "<=" ] -> [ Le ] |