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

7 files changed, 30 insertions, 55 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index efac22bc7..736ed0663 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -30,10 +30,6 @@ open Nametab
 (*Takes a list of variables which must not be globalized*)
 let from_list l = List.fold_right Idset.add l Idset.empty
 
-let rec adjust_implicits n = function
-  | p::l -> if p<=n then adjust_implicits n l else (p-n)::adjust_implicits n l
-  | [] -> []
-
 (* when an head ident is not a constructor in pattern *)
 let mssg_hd_is_not_constructor s =
   [< 'sTR "The symbol "; pr_id s; 'sTR " should be a constructor" >]
@@ -201,26 +197,20 @@ let ast_to_global loc c =
   match c with
     | ("CONST", [sp]) ->
 	let ref = ConstRef (ast_to_sp sp) in
-	let hyps = implicit_section_args ref in
-	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
 	let imps = implicits_of_global ref in
-	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+	RRef (loc, ref), imps
     | ("MUTIND", [sp;Num(_,tyi)]) -> 
 	let ref = IndRef (ast_to_sp sp, tyi) in
-	let hyps = implicit_section_args ref in
-	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
 	let imps = implicits_of_global ref in
-	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+	RRef (loc, ref), imps
     | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) ->
 	let ref = ConstructRef ((ast_to_sp sp,ti),n) in
-	let hyps = implicit_section_args ref in
-	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
 	let imps = implicits_of_global ref in
-	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+	RRef (loc, ref), imps
     | ("EVAR", [(Num (_,ev))]) ->
-	REvar (loc, ev), [], []
+	REvar (loc, ev), []
     | ("SYNCONST", [sp]) ->
-	Syntax_def.search_syntactic_definition (ast_to_sp sp), [], []
+	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
     | _ -> anomaly_loc (loc,"ast_to_global",
 			[< 'sTR "Bad ast for this global a reference">])
 
@@ -251,7 +241,7 @@ let ast_to_var (env,impls) (vars1,vars2) loc id =
 	let ref = VarRef (Lib.make_path id CCI) in
 	implicits_of_global ref
       with _ -> []
-  in RVar (loc, id), [], imps
+  in RVar (loc, id), imps
 
 (**********************************************************************)
 
@@ -271,12 +261,10 @@ let rawconstr_of_qualid env vars loc qid =
   (* Is it a global reference or a syntactic definition? *)
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
-    let hyps = implicit_section_args ref in
-    let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
     let imps = implicits_of_global ref in
-    RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
+    RRef (loc, ref), imps
   | SyntacticDef sp ->
-    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp),[],[]
+    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp), []
   with Not_found ->
     error_global_not_found_loc loc qid
 
@@ -366,12 +354,10 @@ let check_capture loc s ty = function
 let ast_to_rawconstr sigma env allow_soapp lvar =
   let rec dbrec (ids,impls as env) = function
     | Nvar(loc,s) ->
-	let f, hyps, _ = rawconstr_of_var env lvar loc s in
-	if hyps = [] then f else RApp (loc, f, hyps)
+	fst (rawconstr_of_var env lvar loc s)
 
     | Node(loc,"QUALID", l) ->
-	let f, hyps, _ = rawconstr_of_qualid env lvar loc (interp_qualid l) in
-	if hyps = [] then f else RApp (loc, f, hyps)
+        fst (rawconstr_of_qualid env lvar loc (interp_qualid l))
   
     | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
 	let (lf,ln,lA,lt) = ast_to_fix ldecl in
@@ -416,7 +402,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	RApp (loc,dbrec env f,ast_to_args env args)
 
     | Node(loc,"APPLIST", f::args) ->
-	let (c, hyps, impargs) =
+	let (c, impargs) =
 	  match f with
 	    | Node(locs,"QUALID",p) ->
 		rawconstr_of_qualid env lvar locs (interp_qualid p)
@@ -424,9 +410,9 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 		   ("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),
 		   l) ->
 		ast_to_global loc (key,l)
-	    | _ -> (dbrec env f, [], [])
+	    | _ -> (dbrec env f, [])
         in
-	  RApp (loc, c, hyps @ (ast_to_impargs env impargs args))
+	  RApp (loc, c, ast_to_impargs env impargs args)
 
     | Node(loc,"CASES", p:: Node(_,"TOMATCH",tms):: eqns) ->
 	let po = match p with 
@@ -456,8 +442,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	  
     (* This case mainly parses things build in a quotation *)
     | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
-	let f, hyps, _ = ast_to_global loc (key,l) in
-	if hyps = [] then f else RApp (loc, f, hyps)	
+	fst (ast_to_global loc (key,l))
 
     | Node(loc,"CAST", [c1;c2]) ->	   
 	RCast (loc,dbrec env c1,dbrec env c2)
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index dca396ea2..4d3e5ce23 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -51,8 +51,7 @@ let reference dir s =
   with Not_found ->
     anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id)))
 
-let constant dir s =
-  Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s)
+let constant dir s = Declare.constr_of_reference (reference dir s)
 
 type coq_sigma_data = {
   proj1 : constr;
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 2a447a910..6dbaabc1c 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -91,7 +91,7 @@ GEXTEND Gram
       | IDENT "Print" -> <:ast< (PRINT) >>
       | IDENT "Print"; IDENT "Hint"; "*" 
 	                    -> <:ast< (PrintHint) >>
-      | IDENT "Print"; IDENT "Hint"; s = identarg ->
+      | IDENT "Print"; IDENT "Hint"; s = qualidarg ->
           <:ast< (PrintHintId $s) >>
       | IDENT "Print"; IDENT "Hint" ->
           <:ast< (PrintHintGoal) >>
@@ -172,7 +172,8 @@ GEXTEND Gram
       | IDENT "Print"; IDENT "Graph" -> <:ast< (PrintGRAPH) >>
       | IDENT "Print"; IDENT "Classes" -> <:ast< (PrintCLASSES) >>
       | IDENT "Print"; IDENT "Coercions" -> <:ast< (PrintCOERCIONS) >>
-      | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; c = identarg; d = identarg ->
+      | IDENT "Print"; IDENT "Coercion"; IDENT "Paths";
+        c = qualidarg; d = qualidarg ->
           <:ast< (PrintPATH $c $d) >>
 
       | IDENT "SearchIsos"; com = constrarg ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3bec62837..f98746a25 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -214,7 +214,7 @@ GEXTEND Gram
       | ":" -> "" ] ]
   ;
   onescheme:
-    [ [ id = identarg; ":="; dep = dep; indid = identarg; IDENT "Sort";
+    [ [ id = identarg; ":="; dep = dep; indid = qualidarg; IDENT "Sort";
         s = sortarg ->
           <:ast< (VERNACARGLIST $id $dep $indid $s) >> ] ]
   ;
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 7c6dad215..5f804f3f2 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -577,33 +577,23 @@ let print_coercions () =
   [< prlist_with_sep pr_spc
        (fun (_,(_,v)) -> [< print_coercion_value v >]) (coercions()) >]
   
-let cl_of_id id = 
-  match string_of_id id with
-    | "FUNCLASS" -> CL_FUN
-    | "SORTCLASS" -> CL_SORT
-    | _ -> let v = Declare.global_reference CCI id in
-	   let cl,_ = constructor_at_head v in 
-	   cl
-
-let index_cl_of_id id =
+let index_of_class cl =
   try 
-    let cl = cl_of_id id in
-    let i,_ = class_info cl in 
-    i
+    fst (class_info cl)
   with _ -> 
-    errorlabstrm "index_cl_of_id"
-      [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
+    errorlabstrm "index_of_class"
+      [< 'sTR(string_of_class cl); 'sTR" is not a defined class" >]
 
-let print_path_between ids idt = 
-  let i = (index_cl_of_id ids) in
-  let j = (index_cl_of_id idt) in
+let print_path_between cls clt = 
+  let i = index_of_class cls in
+  let j = index_of_class clt in
   let p = 
     try 
       lookup_path_between (i,j) 
     with _ -> 
       errorlabstrm "index_cl_of_id"
-        [< 'sTR"No path between ";'sTR(string_of_id ids); 
-	   'sTR" and ";'sTR(string_of_id ids) >]
+        [< 'sTR"No path between ";'sTR(string_of_class cls); 
+	   'sTR" and ";'sTR(string_of_class clt) >]
   in
   print_path ((i,j),p)
 
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index b84c56634..a50a8371f 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -52,7 +52,7 @@ i*)
 val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
 val print_coercions : unit -> std_ppcmds
-val print_path_between : identifier -> identifier -> std_ppcmds
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
 
 
 val inspect : int -> std_ppcmds
diff --git a/parsing/search.ml b/parsing/search.ml
index e0dc3b7a4..fc069f41e 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -48,7 +48,7 @@ let rec head_const c = match kind_of_term c with
 let crible (fn : global_reference -> env -> constr -> unit) ref =
   let env = Global.env () in
   let imported = Library.opened_modules() in
-  let const = constr_of_reference Evd.empty env ref in 
+  let const = constr_of_reference ref in 
   let crible_rec sp lobj =
     match object_tag lobj with
       | "VARIABLE" ->