Suppression des arguments sur les constantes, inductifs et constructeurs

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

5 files changed, 15 insertions, 12 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index c885242bda..936c39d565 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -146,8 +146,8 @@ let coq_constant d s =
   make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
 
 let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
-let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
-let coq_false = mkMutConstruct (((bool_sp,0),2), [||])
+let coq_true = mkMutConstruct ((bool_sp,0),1)
+let coq_false = mkMutConstruct ((bool_sp,0),2)
 
 let constant s =
   let id = id_of_string s in
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 6a7a70cf3e..d4c3494a8a 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -122,6 +122,7 @@ let eq_pattern =
  
 let (loop_ids : tactic) = fun gl ->
   let rec arec hyps gl =
+    let env = pf_env gl in
     let concl = pf_concl gl in 
     match hyps with
       | [] -> tclIDTAC gl
@@ -135,7 +136,7 @@ let (loop_ids : tactic) = fun gl ->
 	    match pf_matches gl eq_pattern (body_of_type a) with
 	      | [_; _,varphi; _] when isVar varphi ->
 		  let phi = destVar varphi in
-		  if occur_var phi concl then
+		  if Environ.occur_var env phi concl then
 		    tclTHEN (rewriteLR (mkVar id)) (arec al) gl
 		  else
 		    arec al gl
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index 29caf31072..de5d2da7d8 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -107,10 +107,10 @@ let effect_app ren env f args =
  * Also returns its variables *)
 
 let state_coq_ast sign a =
+  let env = Global.env_of_context sign in
   let j =
-    let env = Global.env_of_context sign in
     reraise_with_loc (Ast.loc a) (judgment_of_rawconstr Evd.empty env) a in
-  let ids = global_vars j.uj_val in
+  let ids = global_vars env j.uj_val in
   j.uj_val, j.uj_type, ids
 
 (* [is_pure p] tests wether the program p is an expression or not. *)
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index e227a44599..73d1778ac0 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Term
 open Pattern
+open Environ
 
 open Pmisc
 open Ptype
@@ -61,10 +62,10 @@ let is_mutable_in_env env id =
 let now_vars env c =
   Util.map_succeed 
     (function id -> if is_mutable_in_env env id then id else failwith "caught")
-    (global_vars c)
+    (global_vars (Global.env()) c)
 
 let make_before_after c =
-  let ids = global_vars c in
+  let ids = global_vars (Global.env()) c in
   let al = 
     Util.map_succeed
       (function id -> 
@@ -98,18 +99,18 @@ let make_assoc_list ren env on_prime ids =
     [] ids
 
 let apply_pre ren env c =
-  let ids = global_vars c.p_value in
+  let ids = global_vars (Global.env()) c.p_value in
   let al = make_assoc_list ren env current_var ids in
   { p_assert = c.p_assert; p_name = c.p_name; 
     p_value = subst_in_constr al c.p_value }
 
 let apply_assert ren env c =
-  let ids = global_vars c.a_value in
+  let ids = global_vars (Global.env()) c.a_value in
   let al = make_assoc_list ren env current_var ids in
   { a_name = c.a_name; a_value = subst_in_constr al c.a_value }
  
 let apply_post ren env before c =
-  let ids = global_vars c.a_value in
+  let ids = global_vars (Global.env()) c.a_value in
   let al = 
     make_assoc_list ren env (fun r uid -> var_at_date r before uid) ids in
   { a_name = c.a_name; a_value = subst_in_constr al c.a_value }
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index b00f5c38fc..1381bdf92c 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -13,6 +13,7 @@
 open Util
 open Names
 open Term
+open Environ
 
 open Pmisc
 open Ptype
@@ -53,7 +54,7 @@ let update_post env top ef c =
 	     l
 	 else
 	   l) 
-      [] (global_vars c)
+      [] (global_vars (Global.env()) c)
   in
   subst_in_constr al c
   
@@ -110,7 +111,7 @@ let create_bool_post c =
 let is_bool = function
   | TypePure c ->
       (match kind_of_term (strip_outer_cast c) with
-	 | IsMutInd (op,_) -> Global.string_of_global (IndRef op) = "bool"
+	 | IsMutInd op -> Global.string_of_global (IndRef op) = "bool"
 	 | _ -> false)
   | _ -> false