Suppression option immediate_discharge; nettoyage de Declare et conséquences

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

8 files changed, 32 insertions, 70 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 088e7636a1..6bd773698b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -273,10 +273,6 @@ let add_resolves env sigma clist dbnames =
 	    )))
     dbnames
 
-let global qid =
-  try Nametab.locate qid
-  with Not_found -> Nametab.error_global_not_found_loc dummy_loc qid
-
 (* REM : in most cases hintname = id *)
 let make_unfold (hintname, ref) =
   (Pattern.label_of_ref ref,
@@ -340,7 +336,7 @@ let _ =
 	       (function VARG_IDENTIFIER i -> string_of_id i
 		  | _ -> bad_vernac_args "HintUnfold") l in
       	   fun () -> 
-	     let ref = global qid in
+	     let ref = Nametab.global dummy_loc qid in
 	     add_unfolds [(hintname, ref)] dbnames
        | _-> bad_vernac_args "HintUnfold")
     
@@ -381,13 +377,11 @@ let _ =
 	       let isp = destMutInd (Declare.global_qualified_reference qid) in
 	       let conspaths =
 		 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 = 
 		 array_map_to_list
 		   (fun sp ->
 		      let c = Declare.global_absolute_reference sp in
-		      (basename sp, applist (c, section_args)))
+		      (basename sp, c))
 		   conspaths in
 	       let dbnames = if l = [] then ["core"] else 
 	      	 List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -422,13 +416,11 @@ let _ =
 	     List.map
 	       (function
 		  | VARG_QUALID qid -> 
-		      let ref = global qid in
+		      let ref = Nametab.global dummy_loc qid in
 		      let env = Global.env() in
-		      let c = Declare.constr_of_reference Evd.empty env ref in
-		      let hyps = Declare.implicit_section_args ref in
-		      let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
+		      let c = Declare.constr_of_reference ref in
 		      let _,i = Nametab.repr_qualid qid in
-		      (i, applist (c,section_args))
+		      (i, c)
 		  | _-> bad_vernac_args "HintsResolve") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -445,7 +437,7 @@ let _ =
 	     List.map (function
 			 | VARG_QUALID qid ->
 			     let _,n = Nametab.repr_qualid qid in
-			     (n, global qid)
+			     (n, Nametab.global dummy_loc qid)
 		      	 | _ -> bad_vernac_args "HintsUnfold") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function 
@@ -466,10 +458,8 @@ let _ =
 		      let _,n = Nametab.repr_qualid qid in
 		      let ref = Nametab.locate qid in
 		      let env = Global.env () in
-		      let c = Declare.constr_of_reference Evd.empty env ref in
-		      let hyps = Declare.implicit_section_args ref in
-		      let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
-		      (n, applist (c, section_args))
+		      let c = Declare.constr_of_reference ref in
+		      (n, c)
 		  | _ -> bad_vernac_args "HintsImmediate") lh in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function 
@@ -517,15 +507,10 @@ let fmt_hint_list_for_head c =
       [< 'sTR"For "; pr_ref_label c; 'sTR" -> "; 'fNL;
 	 hOV 0 (prlist fmt_hints_db valid_dbs) >]
 
-let fmt_hint_id id = 
-  try 
-    let c = Declare.global_reference CCI id in
-    fmt_hint_list_for_head (head_of_constr_reference c)
-  with Not_found -> 
-    [< pr_id id; 'sTR " not declared" >]
+let fmt_hint_ref ref = fmt_hint_list_for_head (label_of_ref ref)
 
 (* Print all hints associated to head id in any database *)
-let print_hint_id id =  pPNL(fmt_hint_id id)
+let print_hint_qid qid =  pPNL(fmt_hint_ref (Nametab.global dummy_loc qid))
 
 let fmt_hint_term cl = 
   try 
@@ -607,7 +592,7 @@ let _ =
 let _ = 
   vinterp_add "PrintHintId"
     (function 
-       | [(VARG_IDENTIFIER id)] -> fun () -> print_hint_id id
+       | [(VARG_QUALID qid)] -> fun () -> print_hint_qid qid
        | _ -> bad_vernac_args "PrintHintId")
 
 (**************************************************************************)
@@ -961,7 +946,7 @@ let interp_to_add gl = function
   | Qualid qid ->
       let _,id = Nametab.repr_qualid qid in
       (next_ident_away id (pf_ids_of_hyps gl), 
-       Declare.constr_of_reference Evd.empty (Global.env()) (global qid))
+       Declare.constr_of_reference (Nametab.global dummy_loc qid))
   | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >]
 
 let dyn_superauto l g = 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index dc0393b066..fed7568149 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -100,7 +100,7 @@ let head_in gls indl t =
        
 let inductive_of_qualid gls qid =
   let c = 
-    try Declare.construct_qualified_reference (pf_env gls) qid
+    try Declare.construct_qualified_reference qid
     with Not_found -> Nametab.error_global_not_found qid
   in
   match kind_of_term c with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e497fb114d..6c3ee44d89 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -56,7 +56,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
 	then general_s_rewrite lft2rgt c gl
 	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
-        let hdcncls = string_head hdcncl in 
+        let hdcncls = string_of_inductive hdcncl in 
 	let suffix = Declare.elimination_suffix (elimination_sort_of_goal gl)in
         let elim =
 	  if lft2rgt then
@@ -115,20 +115,12 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
   else
     error "terms does not have convertible types"
 
-(* Only for internal use *)
-let unsafe_replace c2 c1 gl = 
-  let eq        = (pf_parse_const gl "eq")     in
-  let eqt       = (pf_parse_const gl "eqT")    in 
-  let sym_eq    = (pf_parse_const gl "sym_eq") in
-  let sym_eqt   = (pf_parse_const gl "sym_eqT") in
-  abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 true gl
-
-let replace c2 c1 gl = 
-  let eq        = (pf_parse_const gl "eq")     in
-  let eqt       = (pf_parse_const gl "eqT")    in 
-  let sym_eq    = (pf_parse_const gl "sym_eq") in
-  let sym_eqt   = (pf_parse_const gl "sym_eqT") in
-  abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 false gl
+let replace c2 c1 gl =
+  let eq = build_coq_eq_data.eq () in
+  let eq_sym = build_coq_eq_data.sym () in
+  let eqT = build_coq_eqT_data.eq () in
+  let eqT_sym = build_coq_eqT_data.sym () in
+  abstract_replace (eq,eq_sym) (eqT,eqT_sym) c2 c1 false gl
     
 let dyn_replace args gl = 
   match args with 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 1735ebf1a0..b7ec9eb591 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -57,9 +57,6 @@ val conditional_rewrite_in :
 val abstract_replace : 
   constr * constr -> constr * constr -> constr -> constr -> bool -> tactic
 
-(* Only for internal use *)
-val unsafe_replace : constr -> constr -> tactic
-
 val replace   : constr -> constr -> tactic
 val h_replace : constr -> constr -> tactic
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index ae2ed421f6..a3bdf52b99 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -119,9 +119,9 @@ let is_unit_type t = op2bool (match_with_unit_type t)
 
 (* Checks if a given term is an application of an
    inductive binary relation R, so that R has only one constructor
-   stablishing its reflexivity.  *)
+   establishing its reflexivity.  *)
 
-let match_with_equation  t =
+let match_with_equation t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
     | IsMutInd ind -> 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index d19c67c18a..ea9e9d104c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -56,7 +56,7 @@ let global_constant dir s =
 
 let current_constant id =
   try
-    Declare.global_reference CCI id
+    Declare.global_reference id
   with Not_found ->
     anomaly ("Setoid: cannot find "^(string_of_id id))
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a8025f12e..04d7b10c1f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -57,20 +57,13 @@ let get_pairs_from_bindings =
   in 
   List.map pair_from_binding
 
-let rec string_head_bound x = match kind_of_term x with
-  | IsConst cst -> string_of_id (basename cst)
+let string_of_inductive c = 
+  try match kind_of_term c with
   | IsMutInd ind_sp -> 
       let mispec = Global.lookup_mind_specif ind_sp in 
       string_of_id (mis_typename mispec)
-  | 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
-
-let string_head c = 
-  try string_head_bound c with Bound -> error "Bound head variable"
-
+  with Bound -> error "Bound head variable"
 
 let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
@@ -1744,8 +1737,8 @@ let dyn_reflexivity = function
 let symmetry gl =
   match match_with_equation (pf_concl gl) with
     | None -> error "The conclusion is not a substitutive equation" 
-    | Some (hdcncl,args) -> 
-        let hdcncls = string_head hdcncl in
+    | Some (hdcncl,args) ->
+        let hdcncls = string_of_inductive hdcncl in
         begin 
 	  try 
 	    (apply (pf_parse_const gl ("sym_"^hdcncls)) gl)
@@ -1782,9 +1775,9 @@ let dyn_symmetry = function
 
 let transitivity t gl =
   match match_with_equation (pf_concl gl) with
-    | None -> error "The conlcusion is not a substitutive equation" 
+    | None -> error "The conclusion is not a substitutive equation" 
     | Some (hdcncl,args) -> 
-        let hdcncls = string_head hdcncl in
+        let hdcncls = string_of_inductive hdcncl in
         begin
 	  try 
 	    apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl 
@@ -1846,7 +1839,7 @@ let abstract_subproof name tac gls =
     in   (* Faudrait un peu fonctionnaliser cela *)
     let sp = Declare.declare_constant na (ConstantEntry const,strength) in
     let newenv = Global.env() in
-    Declare.constr_of_reference Evd.empty newenv (ConstRef sp)
+    Declare.constr_of_reference (ConstRef sp)
   in
   exact_no_check 
     (applist (lemme,
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8751fcb5cb..7205303b23 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -29,12 +29,7 @@ open Tacticals
 val type_clenv_binding : walking_constraints ->
   constr * constr -> constr substitution  -> constr
 
-(*i
-(* [force_reference c] fails if [c] is not a reference *)
-val force_reference   : constr -> constr
-i*)
-
-val string_head       : constr -> string
+val string_of_inductive : constr -> string
 val head_constr       : constr -> constr list
 val head_constr_bound : constr -> constr list -> constr list
 val bad_tactic_args : string -> tactic_arg list -> 'a