diff options
Diffstat (limited to 'contrib/romega')
| -rw-r--r-- | contrib/romega/const_omega.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index 173c443566..c358e593d6 100644 --- a/contrib/romega/const_omega.ml +++ b/contrib/romega/const_omega.ml @@ -20,14 +20,15 @@ let destructurate t = match Term.kind_of_term c, args with | Term.IsConst sp, args -> Kapp (Names.string_of_id - (Names.basename (Global.sp_of_global (Term.ConstRef sp))),args) + (Names.basename (Global.sp_of_global (Names.ConstRef sp))), + args) | Term.IsMutConstruct csp , args -> Kapp (Names.string_of_id - (Names.basename (Global.sp_of_global (Term.ConstructRef csp))), - args) + (Names.basename (Global.sp_of_global(Names.ConstructRef csp))), + args) | Term.IsMutInd isp, args -> Kapp (Names.string_of_id - (Names.basename (Global.sp_of_global (Term.IndRef isp))),args) + (Names.basename (Global.sp_of_global (Names.IndRef isp))),args) | Term.IsVar id,[] -> Kvar(Names.string_of_id id) | Term.IsProd (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.IsProd (Names.Name _,_,_),[] -> @@ -40,9 +41,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 -> Names.ConstRef sp + | Term.IsMutConstruct csp -> Names.ConstructRef csp + | Term.IsMutInd isp -> Names.IndRef isp | _ -> raise Destruct in Names.basename (Global.sp_of_global ref), args |