diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-12 09:37:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-12 09:37:58 +0000 |
| commit | ade8d5b089ee10d3f17cebcbc883cbc6c7343539 (patch) | |
| tree | cc873bc984f2d6a001a28d8fe77452a60bbcc155 /contrib/romega | |
| parent | 7030dc49d4ddc107d131b2f199a5002a5d8e432e (diff) | |
Déplacement de global_reference dans Names pour pouvoir lier Nametab à grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
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 173c44356..c358e593d 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 |