Suppression des arguments sur les constantes, inductifs et constructeurs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 6 deletions

diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 37fb01a4c..173c44356 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -18,14 +18,14 @@ type result =
 let destructurate t =
   let c, args = Reduction.whd_stack t in
   match Term.kind_of_term c, args with
-    | Term.IsConst (sp,_), args ->
+    | Term.IsConst sp, args ->
 	Kapp (Names.string_of_id
 		(Names.basename (Global.sp_of_global (Term.ConstRef sp))),args)
-    | Term.IsMutConstruct (csp,_) , args ->
+    | Term.IsMutConstruct csp , args ->
 	Kapp (Names.string_of_id
 		(Names.basename (Global.sp_of_global (Term.ConstructRef csp))),
 	      args)
-    | Term.IsMutInd (isp,_), args ->
+    | Term.IsMutInd isp, args ->
 	Kapp (Names.string_of_id
 		(Names.basename (Global.sp_of_global (Term.IndRef isp))),args)
     | Term.IsVar id,[] -> Kvar(Names.string_of_id id)
@@ -40,9 +40,9 @@ let dest_const_apply t =
   let f,args = Reduction.whd_stack t in
   let ref = 
   match Term.kind_of_term f with 
-    | Term.IsConst (sp,_)         -> Term.ConstRef sp
-    | Term.IsMutConstruct (csp,_) -> Term.ConstructRef csp
-    | Term.IsMutInd (isp,_)       -> Term.IndRef isp
+    | Term.IsConst sp         -> Term.ConstRef sp
+    | Term.IsMutConstruct csp -> Term.ConstructRef csp
+    | Term.IsMutInd isp       -> Term.IndRef isp
     | _ -> raise Destruct
   in
   Names.basename (Global.sp_of_global ref), args