diff options
Diffstat (limited to 'contrib/romega/g_romega.ml4')
| -rw-r--r-- | contrib/romega/g_romega.ml4 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4 new file mode 100644 index 00000000..386f7f28 --- /dev/null +++ b/contrib/romega/g_romega.ml4 @@ -0,0 +1,15 @@ +(************************************************************************* + + PROJET RNRT Calife - 2001 + Author: Pierre Crégut - France Télécom R&D + Licence : LGPL version 2.1 + + *************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +open Refl_omega + +TACTIC EXTEND ROmega + [ "ROmega" ] -> [ total_reflexive_omega_tactic ] +END |