diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:19 +0000 |
| commit | b5011fe9c8b410074f2b1299cf83aabed834601f (patch) | |
| tree | eb433f71ae754c1f2526bb55f7eb83bb81300dd4 /contrib/romega | |
| parent | 16d5d84c20cc640be08c3f32cc9bde5cbd3f06dd (diff) | |
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/romega')
| -rw-r--r-- | contrib/romega/ROmega.v | 7 | ||||
| -rw-r--r-- | contrib/romega/g_romega.ml4 | 17 |
2 files changed, 17 insertions, 7 deletions
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v index 6bfc3f187..ba02b232e 100644 --- a/contrib/romega/ROmega.v +++ b/contrib/romega/ROmega.v @@ -8,10 +8,3 @@ Require Omega. Require ReflOmegaCore. - -Grammar tactic simple_tactic : ast := - romega [ "ROmega" ] -> [(ReflOmega)]. - -Syntax tactic level 0: - romega [ (ReflOmega) ] -> ["ROmega"]. - diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4 new file mode 100644 index 000000000..b5203dcb7 --- /dev/null +++ b/contrib/romega/g_romega.ml4 @@ -0,0 +1,17 @@ +(************************************************************************* + + 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*) + +(* $Id$ *) + +open Refl_omega + +TACTIC EXTEND ROmega + [ "ROmega" ] -> [ omega_solver ] +END |