diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-16 14:59:15 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-16 14:59:15 +0000 |
| commit | 0d5a9c97de52f3ba56a9bf54a7177d33aba79ecd (patch) | |
| tree | fd89da1cdfaf9d9474b2998c3cd8cf5847174f97 /plugins/omega | |
| parent | 2beefbc65d2f571da4918d30cf894a81bcf41662 (diff) | |
Use full path for unknown stuff in omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13637 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c36cded17..6bdfea4ad 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -394,11 +394,11 @@ let destructurate_prop t = | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args) | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args) | Const sp, args -> - Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args) + Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args) | Construct csp , args -> - Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args) + Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args) | Ind isp, args -> - Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args) + Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" |