diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-01 13:20:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-01 13:20:02 +0000 |
| commit | 9e6e6202c073fed0e2fc915d7f7e6ce927d55218 (patch) | |
| tree | ed17038b7fc77a5cba80c41616d4d18d66dd51f1 /contrib/omega/coq_omega.ml | |
| parent | afdb9b7fa4a6ce1165b270ffdae4574897aa7c40 (diff) | |
Disparition du type oper mais nouveau type global_reference
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega/coq_omega.ml')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 678bdd8b3..963f41821 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -83,7 +83,7 @@ let resolve_with_bindings_tac (c,lbind) gl = let reduce_to_mind gl t = let rec elimrec t l = - let c, args = whd_castapp_stack t [] in + let c, args = whd_stack t in match kind_of_term c, args with | (IsMutInd _,_) -> (c,Environ.it_mkProd_or_LetIn t l) | (IsConst _,_) -> @@ -162,9 +162,9 @@ exception Destruct let dest_const_apply t = let f,args = get_applist t in match kind_of_term f with - | IsConst (sp,_) -> Global.id_of_global (Const sp),args - | IsMutConstruct (csp,_) -> Global.id_of_global (MutConstruct csp),args - | IsMutInd (isp,_) -> Global.id_of_global (MutInd isp),args + | IsConst (sp,_) -> Global.id_of_global (ConstRef sp),args + | IsMutConstruct (csp,_) -> Global.id_of_global (ConstructRef csp),args + | IsMutInd (isp,_) -> Global.id_of_global (IndRef isp),args | _ -> raise Destruct type result = @@ -177,11 +177,11 @@ let destructurate t = let c, args = get_applist t in match kind_of_term c, args with | IsConst (sp,_), args -> - Kapp (string_of_id (Global.id_of_global (Const sp)),args) + Kapp (string_of_id (Global.id_of_global (ConstRef sp)),args) | IsMutConstruct (csp,_) , args -> - Kapp (string_of_id (Global.id_of_global (MutConstruct csp)),args) + Kapp (string_of_id (Global.id_of_global (ConstructRef csp)),args) | IsMutInd (isp,_), args -> - Kapp (string_of_id (Global.id_of_global (MutInd isp)),args) + Kapp (string_of_id (Global.id_of_global (IndRef isp)),args) | IsVar id,[] -> Kvar(string_of_id id) | IsProd (Anonymous,typ,body), [] -> Kimp(typ,body) | IsProd (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" |