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

6 files changed, 26 insertions, 16 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index b519968a3f..79c73d2d5b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -386,13 +386,17 @@ let mk_clenv_hnf_constr_type_of wc t =
   mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
 
 let mk_clenv_rename_from wc (c,t) = 
-  mk_clenv_from wc (c,rename_bound_var [] t)
+  mk_clenv_from wc (c,rename_bound_var (w_env wc) [] t)
+
+let mk_clenv_rename_from_n wc n (c,t) = 
+  mk_clenv_from_n wc n (c,rename_bound_var (w_env wc) [] t)
     
 let mk_clenv_rename_type_of wc t =
-  mk_clenv_from wc (t,rename_bound_var [] (w_type_of wc t))
+  mk_clenv_from wc (t,rename_bound_var (w_env wc) [] (w_type_of wc t))
     
 let mk_clenv_rename_hnf_constr_type_of wc t =
-  mk_clenv_from wc (t,rename_bound_var [] (w_hnf_constr wc (w_type_of wc t)))
+  mk_clenv_from wc
+    (t,rename_bound_var (w_env wc) [] (w_hnf_constr wc (w_type_of wc t)))
 
 let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t)
 			      
@@ -1068,7 +1072,7 @@ let make_clenv_binding_apply wc n (c,t) lbind =
     let clause = mk_clenv_from_n wc n (c,t) in
     clenv_constrain_missing_args largs clause
   else if lcomargs = 0 then 
-    let clause = mk_clenv_rename_from wc (c,t) in
+    let clause = mk_clenv_rename_from_n wc n (c,t) in
     clenv_match_args lbind clause
   else 
     errorlabstrm "make_clenv_bindings"
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 20eae81114..3b3ce56ea9 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -62,7 +62,9 @@ val unify_0 :
 val collect_metas : constr -> int list
 val mk_clenv : 'a -> constr -> 'a clausenv
 val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
-val mk_clenv_rename_from : 'a -> constr * constr -> 'a clausenv
+val mk_clenv_from_n : 'a -> int -> constr * constr -> 'a clausenv
+val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
+val mk_clenv_rename_from_n : wc -> int -> constr * constr -> wc clausenv
 val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
 val mk_clenv_printable_type_of : wc -> constr -> wc clausenv
 val mk_clenv_type_of : wc -> constr -> wc clausenv
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 9e9d6c8fb9..0256dd600d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -125,7 +125,7 @@ let w_env     wc    = get_env (ids_it wc)
 let w_hyps    wc    = named_context (get_env (ids_it wc))
 let w_ORELSE wt1 wt2 wc = 
   try wt1 wc with e when catchable_exception e -> wt2 wc
-let w_defined_const wc (sp,_) = defined_constant (w_env wc) sp
+let w_defined_const wc sp = defined_constant (w_env wc) sp
 let w_defined_evar wc k      = Evd.is_defined (w_Underlying wc) k
 let w_const_value wc         = constant_value (w_env wc)
 let w_conv_x wc m n          = is_conv (w_env wc) (w_Underlying wc) m n
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 22751eaf9d..58fb852401 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -202,10 +202,11 @@ let split_sign hfrom hto l =
   splitrec [] false l
 
 let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
+  let env = Global.env() in
   let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
     if toleft
-    then occur_var_in_decl hyp2 d
-    else occur_var_in_decl hyp d2
+    then occur_var_in_decl env hyp2 d
+    else occur_var_in_decl env hyp d2
   in
   let rec moverec first middle = function
     | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
@@ -260,9 +261,11 @@ let apply_to_hyp2 env id f =
   if (not !check) || !found then env' else error "No such assumption"
 
 let global_vars_set_of_var = function
-  | (_,None,t) -> global_vars_set (body_of_type t)
+  | (_,None,t) -> global_vars_set (Global.env()) (body_of_type t)
   | (_,Some c,t) ->
-      Idset.union (global_vars_set (body_of_type t)) (global_vars_set c)
+      let env =Global.env() in
+      Idset.union (global_vars_set env (body_of_type t))
+        (global_vars_set env c)
 
 let check_backward_dependencies sign d =
   if not (Idset.for_all
@@ -272,9 +275,10 @@ let check_backward_dependencies sign d =
     error "Can't introduce at that location: free variable conflict"
 
 let check_forward_dependencies id tail =
+  let env = Global.env() in
   List.iter
     (function (id',_,_ as decl) ->
-       if occur_var_in_decl id decl then
+       if occur_var_in_decl env id decl then
 	 error ((string_of_id id) ^ " is used in the hypothesis " 
 		^ (string_of_id id')))
     tail
@@ -529,7 +533,7 @@ let prim_refiner r sigma goal =
 
     | { name = Thin; hypspecs = ids } ->
 	let clear_aux sign id =
-          if !check && occur_var id cl then
+          if !check && occur_var env id cl then
             error ((string_of_id id) ^ " is used in the conclusion.");
           remove_hyp sign id 
 	in
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index ca67f73063..a77fb84a03 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -107,7 +107,7 @@ let make_qid = function
   | VArg (Identifier id) -> VArg (Qualid (make_qualid [] id))
   | VArg (Constr c) ->
     (match (kind_of_term c) with
-    | IsConst _ -> VArg (Qualid (qualid_of_sp (path_of_const c)))
+    | IsConst cst -> VArg (Qualid (qualid_of_sp cst))
     | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >])
   | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >]
 
@@ -1057,7 +1057,7 @@ and cast_opencom_interp ist com =
 and qid_interp ist = function
   | Node(loc,"QUALIDARG",p) -> interp_qualid p
   | Node(loc,"QUALIDMETA",[Num(_,n)]) ->
-    Nametab.qualid_of_sp (path_of_const (List.assoc n ist.lmatch))
+      Nametab.qualid_of_sp (destConst(List.assoc n ist.lmatch))
   | ast -> 
       anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",[<'sTR
         "Unrecognizable qualid ast: "; print_ast ast>])
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5c1a2c8761..8a05e0989b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -276,7 +276,7 @@ let mutual_cofix lf lar pf =
 let rename_bound_var_goal gls =
   let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in 
   let ids = ids_of_named_context sign in
-  convert_concl (rename_bound_var ids cl) gls
+  convert_concl (rename_bound_var (Global.env()) ids cl) gls
     
 
 (***************************************)
@@ -481,7 +481,7 @@ open Pp
 open Printer
 
 let pr_com sigma goal com =
-  prterm (rename_bound_var 
+  prterm (rename_bound_var (Global.env())
             (ids_of_named_context goal.evar_hyps) 
             (Astterm.interp_constr sigma (Evarutil.evar_env goal) com))