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, 43 insertions, 82 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 50c0f33e0d..21e1242f87 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -82,7 +82,7 @@ let rec arity_sort a = match kind_of_term a with
 (* try_add_class : Names.identifier ->
   Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *)
 
-let try_add_class v (cl,p) streopt check_exist = 
+let try_add_class (cl,p) streopt check_exist = 
   if check_exist & class_exists cl then
     errorlabstrm "try_add_new_class" 
       [< 'sTR (string_of_class cl) ; 'sTR " is already a class" >];
@@ -96,7 +96,7 @@ let try_add_class v (cl,p) streopt check_exist =
 (* try_add_new_class : Names.identifier -> unit *)
 
 let try_add_new_class ref stre =
-  let v = constr_of_reference Evd.empty (Global.env()) ref in
+  let v = constr_of_reference ref in
   let env = Global.env () in
   let t = Retyping.get_type_of env Evd.empty v in
   let p1 =
@@ -108,7 +108,7 @@ let try_add_new_class ref stre =
            'sTR " does not end with a sort" >] 
   in
   let cl = fst (constructor_at_head v) in
-  let _ = try_add_class v (cl,p1) (Some stre) true in () 
+  let _ = try_add_class (cl,p1) (Some stre) true in () 
 
 (* Coercions *)
 
@@ -173,7 +173,7 @@ let check_class v cl p =
       with Not_found -> raise (CoercionError (NotAClass cl))
     in
     check_fully_applied cl p p1;
-    try_add_class v (cl,p1) None false
+    try_add_class (cl,p1) None false
 
 (* check that the computed target is the provided one *)
 let check_target clt = function
@@ -294,7 +294,7 @@ let error_not_transparent source =
 let build_id_coercion idf_opt source =
   let env = Global.env () in
   let vs = match source with
-    | CL_CONST sp -> constr_of_reference Evd.empty env (ConstRef sp)
+    | CL_CONST sp -> mkConst sp
     | _ -> error_not_transparent source in
   let c = match Instantiate.constant_opt_value env (destConst vs) with
     | Some c -> c
@@ -349,7 +349,7 @@ lorque source est None alors target est None aussi.
 
 let add_new_coercion_core coef stre source target isid =
   let env = Global.env () in
-  let v = constr_of_reference Evd.empty env coef in
+  let v = constr_of_reference coef in
   let vj = Retyping.get_judgment_of env Evd.empty v in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let lp = prods_of (vj.uj_type) in
@@ -408,7 +408,7 @@ type coercion_entry =
 let add_new_coercion (ref,stre,isid,cls,clt,n) =
   (* Un peu lourd, tout cela pour trouver l'instance *)
   let env = Global.env () in
-  let v = constr_of_reference Evd.empty env ref in
+  let v = constr_of_reference ref in
   let vj = Retyping.get_judgment_of env Evd.empty v in
   declare_coercion ref vj stre isid cls clt n
 
@@ -458,11 +458,6 @@ let process_class sec_sp ids_to_discard x =
           let newsp = Lib.make_path spid CCI in
 	  let hyps = (Global.lookup_constant sp).const_hyps in
 	  let n = count_extra_abstractions hyps ids_to_discard in
-(*
-          let v = global_reference CCI spid in
-          let t = Retyping.get_type_of env Evd.empty v in
-          let p = arity_sort t in
-*)
           (CL_CONST newsp,{cl_strength=stre;cl_param=p+n})
         else 
 	  x
@@ -472,11 +467,6 @@ let process_class sec_sp ids_to_discard x =
           let newsp = Lib.make_path spid CCI in 
 	  let hyps = (Global.lookup_mind sp).mind_hyps in
 	  let n = count_extra_abstractions hyps ids_to_discard in
-(*
-          let v = global_reference CCI spid in
-          let t = Retyping.get_type_of env Evd.empty v in
-          let p = arity_sort t in
-*)
           (CL_IND (newsp,i),{cl_strength=stre;cl_param=p+n})
         else 
 	  x
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b93cc8b6aa..51af38e20e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -308,7 +308,7 @@ let build_recursive lnameargsardef =
   let lrefrec = Array.mapi declare namerec in
   if_verbose pPNL (recursive_message lrefrec);
   (* The others are declared as normal definitions *)
-  let var_subst id = (id, global_reference CCI id) in
+  let var_subst id = (id, global_reference id) in
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
@@ -370,7 +370,7 @@ let build_corecursive lnameardef =
   in 
   let lrefrec = Array.mapi declare namerec in
   if_verbose pPNL (corecursive_message lrefrec);
-  let var_subst id = (id, global_reference CCI id) in
+  let var_subst id = (id, global_reference id) in
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
@@ -385,17 +385,12 @@ let build_corecursive lnameardef =
   in
   ()
 
-let inductive_of_ident id =
-  let c =
-    try global_reference CCI id
-    with Not_found ->
-      errorlabstrm "inductive_of_ident"
-	[< 'sTR ((string_of_id id) ^ " not found") >]
-  in
-  match kind_of_term (global_reference CCI id) with
-    | IsMutInd ind -> ind
-    | _ -> errorlabstrm "inductive_of_ident"
-	[< 'sTR (string_of_id id); 'sPC; 'sTR "is not an inductive type" >]
+let inductive_of_ident qid =
+  match Nametab.global dummy_loc qid with
+    | IndRef ind -> ind
+    | ref -> errorlabstrm "inductive_of_ident"
+	[< 'sTR (Global.string_of_global ref); 
+           'sPC; 'sTR "is not an inductive type">]
 
 let build_scheme lnamedepindsort = 
   let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 63456e33ba..f45dc633fc 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -49,7 +49,7 @@ val build_recursive :
 
 val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
 
-val build_scheme : (identifier * bool * identifier * Coqast.t) list -> unit
+val build_scheme : (identifier * bool * Nametab.qualid * Coqast.t) list -> unit
 
 val start_proof_com : identifier option -> strength -> Coqast.t -> unit
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 9b634bf082..01b868aa23 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -314,16 +314,12 @@ let close_section _ s =
   let newdir = dirpath sec_sp in
   let olddir = wd_of_sp sec_sp in
   let (ops,ids,_) = 
-    if Options.immediate_discharge then ([],[],([],[],[]))
-    else
-      List.fold_left 
-	(process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
+    List.fold_left 
+      (process_item oldenv newdir olddir) ([],[],([],[],[])) decls 
   in
   let ids = last_section_hyps olddir in
   Global.pop_named_decls ids;
   Summary.unfreeze_lost_summaries fs;
   add_frozen_state ();
-  if Options.immediate_discharge then ()
-  else
-    catch_not_found (List.iter process_operation) (List.rev ops);
+  catch_not_found (List.iter process_operation) (List.rev ops);
   Nametab.push_section olddir
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 87cb11b612..a8f90e3ec9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -87,7 +87,7 @@ let declare_projections indsp coers fields =
   let paramdecls = 
     List.map (fun (na,b,t) -> match na with Name id -> (id,b,t) | _ -> assert false)
       paramdecls in
-  let r = constr_of_reference Evd.empty (Global.env()) (IndRef indsp) in
+  let r = mkMutInd indsp in
   let paramargs = List.rev (List.map (fun (id,_,_) -> mkVar id) paramdecls) in
   let rp = applist (r, paramargs) in
   let x = Environ.named_hd (Global.env()) r Anonymous in
@@ -117,7 +117,6 @@ let declare_projections indsp coers fields =
 	     it_mkNamedLambda_or_LetIn (mkLambda (x, rp, body)) paramdecls in
 	   let name = 
 	     try
-	       let proj = instantiate_inductive_section_params proj indsp in
 	       let cie = { const_entry_body = proj;
                            const_entry_type = None;
                            const_entry_opaque = false } in
@@ -132,8 +131,7 @@ let declare_projections indsp coers fields =
 	     | None -> (None::sp_projs, fi::ids_not_ok, subst)
 	     | Some sp ->
 		 let refi = ConstRef sp in
-		 let constr_fi =
-		   constr_of_reference Evd.empty (Global.env()) refi in
+		 let constr_fi = mkConst sp in
 		 if coe then begin
 		   let cl = Class.class_of_ref (IndRef indsp) in
 		   Class.try_add_new_coercion_with_source 
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index ac46427227..dac63126aa 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -45,7 +45,7 @@ let trait t =
 let objdef_declare ref =
   let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
   let env = Global.env () in
-  let v = constr_of_reference Evd.empty env ref in
+  let v = constr_of_reference ref in
   let vc =
     match kind_of_term v with
       | IsConst cst ->
@@ -82,6 +82,6 @@ let objdef_declare ref =
         List.iter 
 	  (fun (spi,(ci,l_ui)) -> 
 	     add_new_objdef 
-	       ((ConstRef spi,cte_of_constr ci),v,lt,params,l_ui)) comp
+	       ((ConstRef spi,reference_of_constr ci),v,lt,params,l_ui)) comp
     | _ -> objdef_err ref
                  
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bdf448afe5..d4d51073d9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -106,21 +106,6 @@ let show_top_evars () =
   let sigma = project gls in 
   mSG (pr_evars_int 1 (Evd.non_instantiated sigma))
 
-(* Locate commands *)
-let locate_qualid loc qid =
-  try Nametab.locate qid
-  with Not_found -> 
-  try
-    let _ = Syntax_def.locate_syntactic_definition qid in
-    error
-      ("Unexpected reference to a syntactic definition: "
-       ^(Nametab.string_of_qualid qid))
-  with Not_found ->
-    Nametab.error_global_not_found_loc loc qid
-
- (* Pour pcoq *)
-let global = locate_qualid
-
 let locate_file f =
   try
     let _,file =
@@ -514,7 +499,7 @@ let _ =
        | _  -> bad_vernac_args "IMPLICIT_ARGS_OFF")
 
 let coercion_of_qualid loc qid =
-  let ref = locate_qualid loc qid in
+  let ref = Nametab.global loc qid in
   let coe = Classops.coe_of_reference ref in
   if not (Classops.coercion_exists coe) then
     errorlabstrm "try_add_coercion" 
@@ -537,10 +522,10 @@ let _ =
 	   (fun () ->
 	      let imps = number_list l in
 	      Impargs.declare_manual_implicits
-		(locate_qualid dummy_loc qid) imps)
+		(Nametab.global dummy_loc qid) imps)
        | [VARG_STRING "Auto"; VARG_QUALID qid] -> 
 	   (fun () -> 
-	      Impargs.declare_implicits (locate_qualid dummy_loc qid))
+	      Impargs.declare_implicits (Nametab.global dummy_loc qid))
        | _  -> bad_vernac_args "IMPLICITS")
 
 let interp_definition_kind = function
@@ -597,7 +582,7 @@ let _ =
        List.iter 
 	 (function 
 	    | VARG_QUALID qid ->
-                (match locate_qualid dummy_loc qid with
+                (match Nametab.global dummy_loc qid with
                   | ConstRef sp -> Opaque.set_transparent_const sp
                   | VarRef sp -> Opaque.set_transparent_var (basename sp) 
                   | _ -> error
@@ -611,7 +596,7 @@ let _ =
        List.iter
 	 (function 
 	    | VARG_QUALID qid ->
-                (match locate_qualid dummy_loc qid with
+                (match Nametab.global dummy_loc qid with
                   | ConstRef sp -> Opaque.set_opaque_const sp
                   | VarRef sp -> Opaque.set_opaque_var (basename sp) 
                   | _ -> error
@@ -1024,7 +1009,7 @@ let _ =
     (function 
        | (VARG_QUALID qid) :: l ->
 	   (fun () ->
-	      let ref = locate_qualid dummy_loc qid in
+	      let ref = Nametab.global dummy_loc qid in
 	      Search.search_by_head ref (inside_outside l))
        | _ -> bad_vernac_args "SEARCH")
 
@@ -1221,7 +1206,7 @@ let _ =
 		  | (VARG_VARGLIST 
 		       [VARG_IDENTIFIER fid;
 			VARG_STRING depstr;
-			VARG_IDENTIFIER indid;
+			VARG_QUALID indid;
 			VARG_CONSTR sort]) ->
 		      let dep = match depstr with 
 			| "DEP" -> true
@@ -1296,7 +1281,7 @@ let _ =
 	       NeverDischarge 
 	   in
 	   fun () -> 
-	     let ref = locate_qualid dummy_loc qid in
+	     let ref = Nametab.global dummy_loc qid in
 	     Class.try_add_new_class ref stre;
              if_verbose message
                ((Nametab.string_of_qualid qid) ^ " is now a class")
@@ -1306,7 +1291,7 @@ let cl_of_qualid qid =
   match Nametab.repr_qualid qid with
     | [], id when string_of_id id = "FUNCLASS" -> Classops.CL_FUN
     | [], id when string_of_id id = "SORTCLASS" -> Classops.CL_SORT
-    | _ -> Class.class_of_ref (locate_qualid dummy_loc qid)	
+    | _ -> Class.class_of_ref (Nametab.global dummy_loc qid)	
 
 let _ =
   add "COERCION"
@@ -1328,7 +1313,7 @@ let _ =
 		   Class.try_add_new_identity_coercion id stre source target
 	       | _ -> bad_vernac_args "COERCION"
 	     else
-	       let ref = locate_qualid dummy_loc qid in
+	       let ref = Nametab.global dummy_loc qid in
 	       Class.try_add_new_coercion_with_target ref stre source target;
 	       if_verbose
 		 message
@@ -1356,8 +1341,10 @@ let _ =
 let _ =
   add "PrintPATH"
     (function 
-       | [VARG_IDENTIFIER ids;VARG_IDENTIFIER idt] -> 
-	   (fun () -> pPNL (Prettyp.print_path_between ids idt))
+       | [VARG_QUALID qids;VARG_QUALID qidt] -> 
+	   (fun () ->
+              pPNL (Prettyp.print_path_between
+                      (cl_of_qualid qids) (cl_of_qualid qidt)))
        | _ -> bad_vernac_args "PrintPATH")
 
 (* Meta-syntax commands *)
@@ -1509,7 +1496,7 @@ let _ =
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#add (locate_qualid dummy_loc v)
+		(get_ident_table key)#add (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING s] -> 
@@ -1524,7 +1511,7 @@ let _ =
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#add (locate_qualid dummy_loc v)
+		(get_ident_table key)#add (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_STRING s] ->
@@ -1558,7 +1545,7 @@ let _ =
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#remove (locate_qualid dummy_loc v)
+		(get_ident_table key)#remove (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> 
@@ -1573,7 +1560,7 @@ let _ =
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#remove (locate_qualid dummy_loc v)
+		(get_ident_table key)#remove (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_STRING v] -> 
@@ -1614,7 +1601,7 @@ let _ =
 	      let key = 
 		SecondaryTable (string_of_id t,string_of_id f) in
 	      try 
-		(get_ident_table key)#mem (locate_qualid dummy_loc v)
+		(get_ident_table key)#mem (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> 
@@ -1629,7 +1616,7 @@ let _ =
 	   (fun () ->
 	      let key = PrimaryTable (string_of_id t) in
 	      try 
-		(get_ident_table key)#mem (locate_qualid dummy_loc v)
+		(get_ident_table key)#mem (Nametab.global dummy_loc v)
 	      with Not_found -> 
 		error_undeclared_key key)
        | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> 
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 6c829e5a26..5aa37beeb2 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -30,11 +30,6 @@ val show_node : unit -> unit
    in the context of the current goal, as for instance in pcoq *)
 val get_current_context_of_args : vernac_arg list -> Proof_type.enamed_declarations * Environ.env
 
-(* This function is used to transform a qualified identifier into a
-   global reference, with a nice error message in case of failure.
-   It is used in pcoq. *)
-val global : Coqast.loc -> Nametab.qualid -> global_reference;;
-
 (* this function is used to analyse the extra arguments in search commands.
    It is used in pcoq. *)
 val inside_outside : vernac_arg list -> dir_path list * bool;;