From b91f60aab99980b604dc379b4ca62f152315c841 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 5 Nov 2001 16:48:30 +0000
Subject: GROS COMMIT:  - reduction du noyau (variables existentielles,
 fonctions auxiliaires    pour inventer des noms, etc. deplacees hors de
 kernel/)  - changement de noms de constructeurs des constr (suppression de
 "Is" et    "Mut")

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/romega/const_omega.ml | 38 ++++++++++++++++++++------------------
 1 file changed, 20 insertions(+), 18 deletions(-)

(limited to 'contrib/romega/const_omega.ml')

diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index c64038323..76a6bdf52 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -16,37 +16,38 @@ type result =
  | Kufo;;
 
 let destructurate t =
-  let c, args = Reduction.whd_stack t in
+  let c, args = Term.decompose_app t in
+  let env = Global.env() in
   match Term.kind_of_term c, args with
-    | Term.IsConst sp, args ->
+    | Term.Const sp, args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global (Names.ConstRef sp))),
-                args)
-    | Term.IsMutConstruct csp , args ->
+		(Termops.id_of_global env (Nametab.ConstRef sp)),
+              args)
+    | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global(Names.ConstructRef csp))),
+		(Termops.id_of_global env (Nametab.ConstructRef csp)),
 	        args)
-    | Term.IsMutInd isp, args ->
+    | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(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 _,_,_),[] ->
+		(Termops.id_of_global env (Nametab.IndRef isp)),args)
+    | Term.Var id,[] -> Kvar(Names.string_of_id id)
+    | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
+    | Term.Prod (Names.Name _,_,_),[] ->
 	Util.error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
 exception Destruct
 
 let dest_const_apply t = 
-  let f,args = Reduction.whd_stack t in
+  let f,args = Term.decompose_app t in
   let ref = 
   match Term.kind_of_term f with 
-    | Term.IsConst sp         -> Names.ConstRef sp
-    | Term.IsMutConstruct csp -> Names.ConstructRef csp
-    | Term.IsMutInd isp       -> Names.IndRef isp
+    | Term.Const sp         -> Nametab.ConstRef sp
+    | Term.Construct csp -> Nametab.ConstructRef csp
+    | Term.Ind isp       -> Nametab.IndRef isp
     | _ -> raise Destruct
   in
-  Names.basename (Global.sp_of_global ref), args
+  Termops.id_of_global (Global.env()) ref, args
 
 let recognize_number t =
   let rec loop t =
@@ -64,8 +65,9 @@ let recognize_number t =
 let constant dir s =
   try
     Declare.global_absolute_reference
-      (Names.make_path (Names.make_dirpath (List.map Names.id_of_string dir))
-                       (Names.id_of_string s) Names.CCI)
+      (Names.make_path
+        (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
+        (Names.id_of_string s))
   with e -> print_endline (String.concat "." dir); print_endline s; 
             raise e
 
-- 
cgit v1.2.3