From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: 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 --- plugins/romega/g_romega.ml4 | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins/romega/g_romega.ml4') 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> | "positive" -> Tacinterp.interp <:tactic> | "N" -> Tacinterp.interp <:tactic> | "Z" -> Tacinterp.interp <:tactic> | 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 -- cgit v1.2.3