nouvel algo de conversion plus uniforme

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 15 insertions, 14 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ec90fc925d..d73264e924 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -11,6 +11,7 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
 open Termops
 open Sign
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 6043857fa5..61edd06bf6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -11,6 +11,7 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Evd
 open Term
 open Termops
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2b8416eaef..b148c019af 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -11,6 +11,7 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Sign
 open Term
 open Declarations
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 809fbd7b84..af106b1c4b 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -11,6 +11,7 @@
 open Closure
 open Util
 open Names
+open Nameops
 open Term
 open Termops
 open Sign
@@ -262,7 +263,7 @@ let rec ast_of_cvt_intro_pattern = function
 (* Gives the ast list corresponding to a reduction flag *)
 open RedFlags
 
-let last_of_cvt_flags (_,red) =
+let last_of_cvt_flags red =
   (if (red_set red fBETA) then [ope("Beta",[])]
    else [])@
   (let (n_unf,lconst) = red_get_const red in
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 32d96bce16..56fe36890a 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -213,14 +213,10 @@ let glob_const_nvar loc env qid =
     (* We first look for a variable of the current proof *)
     match Nametab.repr_qualid qid with
       | d,id when repr_dirpath d = [] ->
-	  (* lookup_value may raise Not_found *)
-	  (match Environ.lookup_named id env with
-	     | (_,Some _,_) ->
-                 let v = EvalVarRef id in
-                 if Opaque.is_evaluable env v then v
-                 else error ("variable "^(string_of_id id)^" is opaque")
-	     | _ -> error ((string_of_id id)^
-			      " does not denote an evaluable constant"))
+          let v = EvalVarRef id in
+          if Tacred.is_evaluable env v then v
+          else error
+            ((string_of_id id^" does not denote an evaluable constant"))
       | _ -> raise Not_found
   with Not_found ->
   try
@@ -229,7 +225,7 @@ let glob_const_nvar loc env qid =
       | VarRef id -> EvalVarRef id
       | _ -> error ((Nametab.string_of_qualid qid) ^
 		    " does not denote an evaluable constant")) in
-    if Opaque.is_evaluable env ev then ev
+    if Tacred.is_evaluable env ev then ev
     else error ((Nametab.string_of_qualid qid) ^
 		    " does not denote an evaluable constant")
   with Not_found ->
@@ -1124,7 +1120,7 @@ and flag_of_ast ist lf =
 	in add_flag red lf
     | Node(_,"Delta",[])::Node(loc,"UnfBut",l)::lf ->
         let red = red_add red fDELTA in
-        let red = red_add_transparent red (Opaque.state()) in
+        let red = red_add_transparent red (Conv_oracle.freeze()) in
         let red =
 	  List.fold_right
 	    (fun v red -> 
@@ -1134,7 +1130,7 @@ and flag_of_ast ist lf =
 	in add_flag red lf
     | Node(_,"Delta",[])::lf ->
         let red = red_add red fDELTA in
-        let red = red_add_transparent red (Opaque.state()) in
+        let red = red_add_transparent red (Conv_oracle.freeze()) in
         add_flag red lf
     | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf
     | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf
@@ -1153,8 +1149,8 @@ and redexp_of_ast ist = function
   | ("Simpl", []) -> Simpl
   | ("Unfold", ul) -> Unfold (List.map (cvt_unfold ist) ul)
   | ("Fold", cl) -> Fold (List.map (cvt_fold ist) cl)
-  | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast ist lf)
-  | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast ist lf)
+  | ("Cbv",lf) -> Cbv(flag_of_ast ist lf)
+  | ("Lazy",lf) -> Lazy(flag_of_ast ist lf)
   | ("Pattern",lp) -> Pattern (List.map (cvt_pattern ist) lp)
   | (s,_) -> invalid_arg ("malformed reduction-expression: "^s)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d8ef207ffa..377893fd27 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -10,6 +10,7 @@
 
 open Util
 open Names
+open Nameops
 open Sign
 open Term
 open Termops