From 589130e87d68227d25800e7506666eaf1d47a25a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Dec 2015 17:30:09 +0100
Subject: Changing the toplevel type of the int_or_var generic type to int.

---
 plugins/micromega/g_micromega.ml4 | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 62f0ae5037..3c46e1eea0 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -21,12 +21,8 @@ open Misctypes
 
 DECLARE PLUGIN "micromega_plugin"
 
-let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | ArgArg x -> x
-
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) ] -> [  (Coq_micromega.psatz_Z (out_arg i)) ]
+| [ "psatz_Z" int_or_var(i) ] -> [  (Coq_micromega.psatz_Z i) ]
 | [ "psatz_Z" ] -> [  (Coq_micromega.psatz_Z (-1)) ]
 END
 
@@ -63,12 +59,12 @@ TACTIC EXTEND LRA_R
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) ] -> [   (Coq_micromega.psatz_R (out_arg i)) ]
+| [ "psatz_R" int_or_var(i) ] -> [   (Coq_micromega.psatz_R i) ]
 | [ "psatz_R" ] -> [   (Coq_micromega.psatz_R (-1)) ]
 END
 
 TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) ] -> [  (Coq_micromega.psatz_Q (out_arg i)) ]
+| [ "psatz_Q" int_or_var(i) ] -> [  (Coq_micromega.psatz_Q i) ]
 | [ "psatz_Q" ] -> [  (Coq_micromega.psatz_Q (-1)) ]
 END
 
-- 
cgit v1.2.3