From 9e6e6202c073fed0e2fc915d7f7e6ce927d55218 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 1 Oct 2000 13:20:02 +0000 Subject: 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 --- contrib/omega/coq_omega.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'contrib/omega/coq_omega.ml') 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" -- cgit v1.2.3