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

9 files changed, 47 insertions, 42 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 742a6ad238..088e7636a1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -378,10 +378,9 @@ let _ =
 	   begin 
 	     try
 	       let env = Global.env() and sigma = Evd.empty in
-	       let (isp, _ as rectype) =
-		 destMutInd (Declare.global_qualified_reference qid) in
+	       let isp = destMutInd (Declare.global_qualified_reference qid) in
 	       let conspaths =
-		 mis_conspaths (Global.lookup_mind_specif rectype) in
+		 mis_conspaths (Global.lookup_mind_specif isp) in
 	       let hyps = Declare.implicit_section_args (IndRef isp) in
 	       let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
 	       let lcons = 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ffdc962a12..dc0393b066 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -12,6 +12,7 @@ open Pp
 open Util
 open Names
 open Term
+open Environ
 open Reduction
 open Inductive
 open Proof_type
@@ -160,7 +161,7 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHyp
        (fun id gls ->
 	  let idty = pf_type_of gls (mkVar id) in
-	  let fvty = global_vars idty in
+	  let fvty = global_vars (pf_env gls) idty in
 	  let possible_bring_ids =
 	    (List.tl (nLastHyps (abs_j - abs_i) gls))
             @bargs.assums in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c2c21d9fd5..e497fb114d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -273,7 +273,7 @@ let find_eq_pattern aritysort sort =
  *)
 
 exception DiscrFound of
-  (constructor_path * int) list * constructor_path * constructor_path
+  (constructor * int) list * constructor * constructor
 
 let find_positions env sigma t1 t2 =
   let rec findrec posn t1 t2 =
@@ -281,7 +281,7 @@ let find_positions env sigma t1 t2 =
     let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
     match (kind_of_term hd1, kind_of_term hd2) with
   	
-      | IsMutConstruct (sp1,_), IsMutConstruct (sp2,_) ->
+      | IsMutConstruct sp1, IsMutConstruct sp2 ->
         (* both sides are constructors, so either we descend, or we can
            discriminate here. *)
 	  if sp1 = sp2 then
@@ -1192,7 +1192,7 @@ let rec eq_mod_rel l_meta t0 t1 =
 let is_hd_const c = match kind_of_term c with
   | IsApp (f,args) ->
       (match kind_of_term f with
-         | IsConst (c,_) -> Some (c, args)
+         | IsConst c -> Some (c, args)
          |_ -> None)
   | _ -> None
 
@@ -1218,7 +1218,7 @@ let sub_term_with_unif cref ceq =
     | OpApp, cl -> begin
 	let f, args = destApplication u in
 	match kind_of_term f with
-          | IsConst (sp,_) when sp = hdsp -> begin
+          | IsConst sp when sp = hdsp -> begin
 	      try (array_fold_left2 eq_mod_rel l_meta args t_args, nb_occ+1)
 	      with NotEqModRel ->
 		Array.fold_left
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 3fbe8e8eef..15e8ee6b32 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -189,7 +189,9 @@ let rec dependent_hyps id idlist sign =
     | [] -> []
     | (id1::l) -> 
 	let id1ty = snd (lookup_named id1 sign) in  
-	if occur_var id (body_of_type id1ty) then id1::dep_rec l else dep_rec l
+	if occur_var (Global.env()) id (body_of_type id1ty)
+        then id1::dep_rec l
+        else dep_rec l
   in 
   dep_rec idlist 
 
@@ -201,8 +203,9 @@ let generalizeRewriteIntros tac depids id gls =
   gls
 
 let var_occurs_in_pf gl id =
-  occur_var id (pf_concl gl) or
-  List.exists (fun (_,t) -> occur_var id t) (pf_hyps_types gl)
+  let env = pf_env gl in
+  occur_var env id (pf_concl gl) or
+  List.exists (fun (_,t) -> occur_var env id t) (pf_hyps_types gl)
 
 let split_dep_and_nodep idl gl =
   (List.filter (var_occurs_in_pf gl) idl,
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 31dddc0387..f6b2ba06f2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -83,14 +83,15 @@ let no_inductive_inconstr env constr =
 
  *)
  
-let thin_ids (hyps,vars) =
+let thin_ids env (hyps,vars) =
   fst
     (List.fold_left
        (fun ((ids,globs) as sofar) (id,c,a) ->
           if List.mem id globs then
 	    match c with
-	      | None -> (id::ids,(global_vars a)@globs)
-	      | Some body -> (id::ids,(global_vars body)@(global_vars a)@globs)
+	      | None -> (id::ids,(global_vars env a)@globs)
+	      | Some body ->
+                  (id::ids,(global_vars env body)@(global_vars env a)@globs)
           else sofar)
        ([],vars) hyps)
 
@@ -167,7 +168,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       pty,goal
     else
       let i = mkAppliedInd ind in
-      let ivars = global_vars i in
+      let ivars = global_vars env i in
       let revargs,ownsign =
 	fold_named_context
 	  (fun env (id,_,_ as d) (revargs,hyps) ->
@@ -201,7 +202,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   in
   assert 
     (list_subset 
-       (global_vars invGoal) 
+       (global_vars env invGoal) 
        (ids_of_named_context (named_context invEnv)));
   (*
     errorlabstrm "lemma_inversion"
@@ -252,7 +253,7 @@ let inversion_lemma_from_goal n na id sort dep_option inv_op =
   let gl = nth_goal_of_pftreestate n pts in
   let t = pf_get_hyp_typ gl id in
   let env = pf_env gl and sigma = project gl in
-  let fv = global_vars t in
+  let fv = global_vars env t in
 (* Pourquoi ??? 
   let thin_ids = thin_ids (hyps,fv) in
   if not(list_subset thin_ids fv) then
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 10dcee8d7c..d19c67c18a 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -292,9 +292,9 @@ let check_is_dependent t n =
 
 let gen_lem_name m = match kind_of_term m with 
   | IsVar id -> add_suffix id "_ext"
-  | IsConst (sp, _) -> add_suffix (basename sp) "_ext"
-  | IsMutInd ((sp, i), _) -> add_suffix (basename sp) ((string_of_int i)^"_ext")
-  | IsMutConstruct (((sp,i),j), _) -> add_suffix
+  | IsConst sp -> add_suffix (basename sp) "_ext"
+  | IsMutInd (sp, i) -> add_suffix (basename sp) ((string_of_int i)^"_ext")
+  | IsMutConstruct ((sp,i),j) -> add_suffix
       (basename sp) ((string_of_int i)^(string_of_int i)^"_ext")
   | _ -> errorlabstrm "New Morphism" [< 'sTR "The term "; prterm m; 'sTR "is not a known name">]
 
@@ -617,9 +617,7 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
       let al = [|hh; cc|] in
       let a = [|hhm; ccm|] in
       let fleche_constr = (Lazy.force coq_fleche) in
-      let fleche_cp = (match (kind_of_term fleche_constr) with
-			 | (IsConst (cp,_)) -> cp 
-			 | _ -> assert false) in
+      let fleche_cp = destConst fleche_constr in
       let new_concl = (mkApp (fleche_constr, al)) in
 	if is_r 
 	then
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 168cd94e1c..d9919b7e0d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -298,7 +298,7 @@ let case_sign ity i =
   analrec [] recarg.(i-1)
 
 let elim_sign ity i =
-  let (_,j),_ = ity in
+  let (_,j) = ity in
   let rec analrec acc = function 
     | (Param(_)::rest) -> analrec (false::acc) rest
     | (Norec::rest)    -> analrec (false::acc) rest
@@ -346,7 +346,7 @@ let general_elim_then_using
       | _ ->
 	  let name_elim =
 	    match kind_of_term elim with
-	      | IsConst (sp,_) -> string_of_path sp
+	      | IsConst sp -> string_of_path sp
 	      | IsVar id -> string_of_id id
 	      | _ -> "\b"
 	  in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 441cb2aad7..e7673944ea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -58,12 +58,12 @@ let get_pairs_from_bindings =
   List.map pair_from_binding
 
 let rec string_head_bound x = match kind_of_term x with
-  | IsConst _ -> string_of_id (basename (path_of_const x))
-  | IsMutInd (ind_sp,args) -> 
-      let mispec = Global.lookup_mind_specif (ind_sp,args) in 
+  | IsConst cst -> string_of_id (basename cst)
+  | IsMutInd ind_sp -> 
+      let mispec = Global.lookup_mind_specif ind_sp in 
       string_of_id (mis_typename mispec)
-  | IsMutConstruct ((ind_sp,i),args) ->
-       let mispec = Global.lookup_mind_specif (ind_sp,args) in 
+  | IsMutConstruct (ind_sp,i) ->
+       let mispec = Global.lookup_mind_specif ind_sp in 
        string_of_id (mis_consnames mispec).(i-1)
   | IsVar id -> string_of_id id
   | _ -> raise Bound
@@ -469,7 +469,7 @@ let move_to_rhyp rhyp gl =
     | (hyp,c,typ) as ht :: rest ->
 	if Some hyp = rhyp then 
 	  lastfixed
-	else if List.exists (occur_var_in_decl hyp) depdecls then 
+	else if List.exists (occur_var_in_decl (pf_env gl) hyp) depdecls then 
 	  get_lhyp lastfixed (ht::depdecls) rest
         else
 	  get_lhyp (Some hyp) depdecls rest
@@ -660,10 +660,11 @@ let generalize_goal gl c cl =
 	  prod_name (Global.env()) (Anonymous, t, cl')
 
 let generalize_dep c gl =
+  let env = pf_env gl in
   let sign = pf_hyps gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
   let rec seek toquant d =
-    if List.exists (fun (id,_,_) -> occur_var_in_decl id d) toquant
+    if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant
       or dependent_in_decl c d then 
       d::toquant
     else 
@@ -680,7 +681,7 @@ let generalize_dep c gl =
   in
   let cl' = List.fold_right mkNamedProd_or_LetIn to_quantify (pf_concl gl) in
   let cl'' = generalize_goal gl c cl' in
-  let args = instance_from_named_context to_quantify in
+  let args = Array.to_list (instance_from_named_context to_quantify) in
   tclTHEN
     (apply_type cl'' (c::args))
     (thin (List.rev tothin'))
@@ -769,7 +770,7 @@ let letin_tac with_eq name c occs gl =
   let (depdecls,marks,ccl)= letin_abstract id c occs gl in 
   let t = pf_type_of gl c in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
-  let args = instance_from_named_context depdecls in
+  let args = Array.to_list (instance_from_named_context depdecls) in
   let newcl = mkNamedLetIn id c t tmpcl in
 (*
     if with_eq then
@@ -1076,7 +1077,7 @@ let default_elim (c,lbindc)  gl =
   let elimc =
     try lookup_eliminator env ind s 
     with Not_found -> 
-      let dir, base,k = repr_path (path_of_inductive_path (fst ind)) in
+      let dir, base,k = repr_path (path_of_inductive_path ind) in
       let id = make_elimination_ident base s in
       errorlabstrm "default_elim"
 	[< 'sTR "Cannot find the elimination combinator :";
@@ -1129,7 +1130,7 @@ comes from a canonically generated one *)
 
 let rec is_rec_arg env sigma indpath t =
   try
-    let ((ind_sp,_),_) = find_mrectype env sigma t in
+    let (ind_sp,_) = find_mrectype env sigma t in
     Declare.path_of_inductive_path ind_sp = indpath
   with Induc -> 
     false
@@ -1211,7 +1212,7 @@ let atomize_param_of_ind hyp0 gl =
       let argl = snd (decomp_app indtyp) in
       let c = List.nth argl (i-1) in
       match kind_of_term c with
-	| IsVar id when not (List.exists (occur_var id) avoid) ->
+	| IsVar id when not (List.exists (occur_var (pf_env gl) id) avoid) ->
 	    atomize_one (i-1) ((mkVar id)::avoid) gl
 	| IsVar id ->
 	    let x = fresh_id [] id gl in
@@ -1239,7 +1240,8 @@ let find_atomic_param_of_ind mind indtyp =
   let indvars = ref Idset.empty in
   for i = nparams to (Array.length argv)-1 do
     match kind_of_term argv.(i) with
-      | IsVar id when not (List.exists (occur_var id) params) -> 
+      | IsVar id
+          when not (List.exists (occur_var (Global.env()) id) params) -> 
 	  indvars := Idset.add id !indvars
       | _ -> ()
   done;
@@ -1323,8 +1325,9 @@ let cook_sign hyp0 indvars env =
       indhyps := hyp::!indhyps; 
       rhyp
     end else
-      if (List.exists (fun id -> occur_var_in_decl id decl) allindhyps
-	  or List.exists (fun (id,_,_) -> occur_var_in_decl id decl) !decldeps)
+      if (List.exists (fun id -> occur_var_in_decl env id decl) allindhyps
+	  or List.exists (fun (id,_,_) -> occur_var_in_decl env id decl)
+        !decldeps)
       then begin
 	decldeps := decl::!decldeps;
 	if !before then 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 4de0a8e46b..6672e56c4f 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -51,8 +51,8 @@ let constr_val_discr t =
   let c, l = decomp t in
   match kind_of_term c with
     (* IsConst _,_) -> Some(TERM c,l) *)
-    | IsMutInd (ind_sp,_) -> Some(IndNode ind_sp,l)
-    | IsMutConstruct (cstr_sp,_) -> Some(CstrNode cstr_sp,l)
+    | IsMutInd ind_sp -> Some(IndNode ind_sp,l)
+    | IsMutConstruct cstr_sp -> Some(CstrNode cstr_sp,l)
     (* Ici, comment distinguer SectionVarNode de VarNode ?? *)
     | IsVar id -> Some(VarNode id,l)
     | _ -> None