aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/g_romega.ml4
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/romega/g_romega.ml4
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/romega/g_romega.ml4')
-rw-r--r--plugins/romega/g_romega.ml416
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 39b6c2106..2db86e005 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -11,23 +11,23 @@
open Refl_omega
open Refiner
-let romega_tactic l =
- let tacs = List.map
- (function
+let romega_tactic l =
+ let tacs = List.map
+ (function
| "nat" -> Tacinterp.interp <:tactic<zify_nat>>
| "positive" -> Tacinterp.interp <:tactic<zify_positive>>
| "N" -> Tacinterp.interp <:tactic<zify_N>>
| "Z" -> Tacinterp.interp <:tactic<zify_op>>
| s -> Util.error ("No ROmega knowledge base for type "^s))
(Util.list_uniquize (List.sort compare l))
- in
+ in
tclTHEN
(tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
- (tclTHEN
- (* because of the contradiction process in (r)omega,
+ (tclTHEN
+ (* because of the contradiction process in (r)omega,
we'd better leave as little as possible in the conclusion,
for an easier decidability argument. *)
- Tactics.intros
+ Tactics.intros
total_reflexive_omega_tactic)
@@ -36,7 +36,7 @@ TACTIC EXTEND romega
END
TACTIC EXTEND romega'
-| [ "romega" "with" ne_ident_list(l) ] ->
+| [ "romega" "with" ne_ident_list(l) ] ->
[ romega_tactic (List.map Names.string_of_id l) ]
| [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ]
END