aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/romega/const_omega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/romega/const_omega.ml')
-rw-r--r--contrib/romega/const_omega.ml12
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