meilleure presentation des commentaires du traducteur

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

6 files changed, 88 insertions, 81 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 57a187f13..44d1bfa1e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -250,8 +250,8 @@ let corecursive_message v =
 
 let interp_mutual lparams lnamearconstrs finite = 
   let allnames = 
-    List.fold_left 
-      (fun acc (id,_,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in
+    List.fold_left (fun acc (id,_,_,l) -> id::(List.map fst l)@acc)
+      [] lnamearconstrs in
   if not (list_distinct allnames) then
     error "Two inductive objects have the same name";
   let nparams = local_binders_length lparams
@@ -288,7 +288,8 @@ let interp_mutual lparams lnamearconstrs finite =
   let paramassums = 
     List.fold_right (fun d l -> match d with
 	(id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in
-  let indnames = List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
+  let indnames =
+    List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
   let nparamassums = List.length paramassums in
   let (ind_env,ind_impls,arityl) =
     List.fold_left
@@ -327,7 +328,6 @@ let interp_mutual lparams lnamearconstrs finite =
     List.map2
       (fun ar (name,_,_,lname_constr) ->
 	 let constrnames, bodies = List.split lname_constr in
-
          (* Compute the conclusions of constructor types *)
 	 (* for inductive given in ML syntax *)
 	 let nar = 
@@ -377,15 +377,15 @@ let eq_la d1 d2 = match d1,d2 with
 
 let extract_coe lc =
   List.fold_right
-    (fun (addcoe,(id,t)) (l1,l2) ->
+    (fun (addcoe,((_,(id:identifier)),t)) (l1,l2) ->
       ((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[])
 
 let extract_coe_la_lc = function
   | []            -> anomaly "Vernacentries: empty list of inductive types"
-  | (id,ntn,la,ar,lc)::rest ->
+  | ((_,id),ntn,la,ar,lc)::rest ->
       let rec check = function 
 	| []             -> [],[]
-  	| (id,ntn,la',ar,lc)::rest ->
+  	| ((_,id),ntn,la',ar,lc)::rest ->
             if (List.length la = List.length la') && 
                (List.for_all2 eq_la la la')
 	    then
@@ -401,7 +401,7 @@ let extract_coe_la_lc = function
       (coes,la,(id,ntn,ar,lc'):: mspec)
 
 let build_mutual lind finite =
-  let (coes,lparams,lnamearconstructs) = extract_coe_la_lc lind in
+  let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in
   let notations,mie = interp_mutual lparams lnamearconstructs finite in
   let kn = declare_mutual_with_eliminations mie in
   (* Declare the notations now bound to the inductive types *)
@@ -578,7 +578,7 @@ let build_corecursive lnameardef =
   in ()
 
 let build_scheme lnamedepindsort = 
-  let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort
+  let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
   and sigma = Evd.empty
   and env0 = Global.env() in
   let lrecspec =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index c12a49485..07faea0b0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -47,7 +47,7 @@ val build_recursive : (fixpoint_expr * decl_notation) list -> unit
 
 val build_corecursive : cofixpoint_expr list -> unit
 
-val build_scheme : (identifier * bool * reference * rawsort) list -> unit
+val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
 
 val generalize_rawconstr : constr_expr -> local_binder list -> constr_expr
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index aab5bc337..a2a679cb1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -35,8 +35,8 @@ open Topconstr
 let name_of id = if id = wildcard then Anonymous else Name id
 
 let interp_decl sigma env = function
-  | Vernacexpr.AssumExpr(id,t) -> (name_of id,None,interp_type Evd.empty env t)
-  | Vernacexpr.DefExpr(id,c,t) ->
+  | Vernacexpr.AssumExpr((_,id),t) -> (name_of id,None,interp_type Evd.empty env t)
+  | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
 	| Some t -> mkCastC (c,t)
@@ -207,10 +207,12 @@ let declare_projections indsp coers fields =
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
    list telling if the corresponding fields must me declared as coercion *)
-let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) =
+let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let coers,fs = List.split cfs in
   let nparams = local_binders_length ps in
-  let extract_name = function Vernacexpr.AssumExpr(id,_) -> id | Vernacexpr.DefExpr (id,_,_) -> id in
+  let extract_name = function
+      Vernacexpr.AssumExpr((_,id),_) -> id
+    | Vernacexpr.DefExpr ((_,id),_,_) -> id in
   let allnames =  idstruc::(List.map extract_name fs) in
   if not (list_distinct allnames) then error "Two objects have the same name";
   (* Now, younger decl in params and fields is on top *)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 45d6e69ba..5837b5a4c 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -24,5 +24,5 @@ val declare_projections :
   inductive -> bool list -> rel_context -> constant option list
 
 val definition_structure :
-  identifier with_coercion * local_binder list *
+  lident with_coercion * local_binder list *
   (local_decl_expr with_coercion) list * identifier * sorts -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f0efb9db8..58eb42b6d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -286,8 +286,8 @@ let vernac_end_proof = function
     if_verbose show_script ();
     match idopt with
     | None -> save_named is_opaque
-    | Some (id,None) -> save_anonymous is_opaque id
-    | Some (id,Some kind) -> save_anonymous_with_strength kind is_opaque id
+    | Some ((_,id),None) -> save_anonymous is_opaque id
+    | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
 
   (* A stupid macro that should be replaced by ``Exact c. Save.'' all along
      the theories [??] *)
@@ -297,7 +297,8 @@ let vernac_exact_proof c =
   save_named true
 
 let vernac_assumption kind l =
-  List.iter (fun (is_coe,(id,c)) -> declare_assumption id is_coe kind [] c) l
+  List.iter (fun (is_coe,((_,id),c)) ->
+              declare_assumption id is_coe kind [] c) l
 
 let vernac_inductive f indl = build_mutual indl f
 
@@ -441,8 +442,8 @@ let vernac_end_modtype id =
 
 let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
-    | None -> add_prefix "Build_" (snd struc)
-    | Some id -> id in
+    | None -> add_prefix "Build_" (snd (snd struc))
+    | Some (_,id) -> id in
   let sigma = Evd.empty in
   let env = Global.env() in
   let s = interp_constr sigma env sort in
@@ -1142,8 +1143,8 @@ let interp c = match c with
       vernac_notation local c infpl mv8 sc
 
   (* Gallina *)
-  | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
-  | VernacStartTheoremProof (k,id,t,top,f) ->
+  | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
+  | VernacStartTheoremProof (k,(_,id),t,top,f) ->
       vernac_start_proof k (Some id) t top f
   | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
@@ -1154,24 +1155,24 @@ let interp c = match c with
   | VernacScheme l -> vernac_scheme l
 
   (* Modules *)
-  | VernacDeclareModule (id,bl,mtyo,mexpro) -> 
+  | VernacDeclareModule ((_,id),bl,mtyo,mexpro) -> 
       vernac_declare_module id bl mtyo mexpro
-  | VernacDefineModule (id,bl,mtyo,mexpro) -> 
+  | VernacDefineModule ((_,id),bl,mtyo,mexpro) -> 
       vernac_define_module id bl mtyo mexpro
-  | VernacDeclareModuleType (id,bl,mtyo) -> 
+  | VernacDeclareModuleType ((_,id),bl,mtyo) -> 
       vernac_declare_module_type id bl mtyo
 
   (* Gallina extensions *)
-  | VernacBeginSection id -> vernac_begin_section id
+  | VernacBeginSection (_,id) -> vernac_begin_section id
 
-  | VernacEndSegment id -> vernac_end_segment id
+  | VernacEndSegment (_,id) -> vernac_end_segment id
 
   | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
   | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
   | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t
-  | VernacIdentityCoercion (str,id,s,t) -> vernac_identity_coercion str id s t
+  | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
 
   (* Solving *)
   | VernacSolve (n,tac,b) -> vernac_solve n tac b
@@ -1197,7 +1198,7 @@ let interp c = match c with
   (* Commands *)
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
-  | VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n
+  | VernacSyntacticDefinition ((_,id),c,n) -> vernac_syntactic_definition id c n
   | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 76d16862a..fe07a53d5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -25,6 +25,10 @@ exception Quit
 open Libnames
 open Nametab
 
+type lident = identifier located
+type lstring = string
+type lreference = reference
+
 type class_rawexpr = FunClass | SortClass | RefClass of reference
   
 type printable =
@@ -131,11 +135,11 @@ type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
 type sort_expr = Rawterm.rawsort
 
 type decl_notation = (string * constr_expr * scope_name option) option
-type simple_binder = identifier * constr_expr
+type simple_binder = lident * constr_expr
 type 'a with_coercion = coercion_flag * 'a
 type constructor_expr = simple_binder with_coercion
 type inductive_expr =
-     identifier * decl_notation * local_binder list * constr_expr
+     lident * decl_notation * local_binder list * constr_expr
     * constructor_expr list
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
@@ -143,47 +147,47 @@ type definition_expr =
       * constr_expr option
 
 type local_decl_expr =
-  | AssumExpr of identifier * constr_expr
-  | DefExpr of identifier * constr_expr * constr_expr option
+  | AssumExpr of lident * constr_expr
+  | DefExpr of lident * constr_expr * constr_expr option
 
-type module_binder = identifier list * module_type_ast
+type module_binder = lident list * module_type_ast
 
 type proof_end =
   | Admitted
-  | Proved of opacity_flag * (identifier * theorem_kind option) option
+  | Proved of opacity_flag * (lident * theorem_kind option) option
 
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
-  | VernacLoad of verbose_flag * string
+  | VernacLoad of verbose_flag * lstring
   | VernacTime of vernac_expr
-  | VernacVar of identifier
+  | VernacVar of lident
 
   (* Syntax *) 
-  | VernacGrammar of string * raw_grammar_entry list
+  | VernacGrammar of lstring * raw_grammar_entry list
   | VernacTacticGrammar of
-      (string * (string * grammar_production list) * raw_tactic_expr) list
-  | VernacSyntax of string * raw_syntax_entry list
+      (lstring * (lstring * grammar_production list) * raw_tactic_expr) list
+  | VernacSyntax of lstring * raw_syntax_entry list
   | VernacSyntaxExtension of locality_flag *
-      (string * syntax_modifier list) option 
-      * (string * syntax_modifier list) option
+      (lstring * syntax_modifier list) option 
+      * (lstring * syntax_modifier list) option
   | VernacDistfix of locality_flag *
-      grammar_associativity * precedence * string * reference *
+      grammar_associativity * precedence * lstring * lreference *
       scope_name option
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
-  | VernacDelimiters of scope_name * string
+  | VernacDelimiters of scope_name * lstring
   | VernacBindScope of scope_name * class_rawexpr list
-  | VernacArgumentsScope of reference * scope_name option list
-  | VernacInfix of locality_flag * (string * syntax_modifier list) *
-      reference * (string * syntax_modifier list) option * scope_name option
+  | VernacArgumentsScope of lreference * scope_name option list
+  | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
+      lreference * (lstring * syntax_modifier list) option * scope_name option
   | VernacNotation of
-      locality_flag * constr_expr * (string * syntax_modifier list) option *
-      (string * syntax_modifier list) option * scope_name option
+      locality_flag * constr_expr * (lstring * syntax_modifier list) option *
+      (lstring * syntax_modifier list) option * scope_name option
 
   (* Gallina *)
-  | VernacDefinition of definition_kind * identifier * definition_expr * 
+  | VernacDefinition of definition_kind * lident * definition_expr * 
       declaration_hook
-  | VernacStartTheoremProof of theorem_kind * identifier *
+  | VernacStartTheoremProof of theorem_kind * lident *
       (local_binder list * constr_expr) * bool * declaration_hook
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
@@ -191,28 +195,28 @@ type vernac_expr =
   | VernacInductive of inductive_flag * inductive_expr list
   | VernacFixpoint of (fixpoint_expr * decl_notation) list
   | VernacCoFixpoint of cofixpoint_expr list
-  | VernacScheme of (identifier * bool * reference * sort_expr) list
+  | VernacScheme of (lident * bool * lreference * sort_expr) list
 
   (* Gallina extensions *)
   | VernacRecord of bool (* = Record or Structure *)
-      * identifier with_coercion * local_binder list
-      * constr_expr * identifier option * local_decl_expr with_coercion list
-  | VernacBeginSection of identifier
-  | VernacEndSegment of identifier
+      * lident with_coercion * local_binder list
+      * constr_expr * lident option * local_decl_expr with_coercion list
+  | VernacBeginSection of lident
+  | VernacEndSegment of lident
   | VernacRequire of
-      export_flag option * specif_flag option * reference list
-  | VernacImport of export_flag * reference list
-  | VernacCanonical of reference
-  | VernacCoercion of strength * reference * class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of strength * identifier * 
+      export_flag option * specif_flag option * lreference list
+  | VernacImport of export_flag * lreference list
+  | VernacCanonical of lreference
+  | VernacCoercion of strength * lreference * class_rawexpr * class_rawexpr
+  | VernacIdentityCoercion of strength * lident * 
       class_rawexpr * class_rawexpr
 
   (* Modules and Module Types *)
-  | VernacDeclareModule of identifier * 
+  | VernacDeclareModule of lident * 
       module_binder list * (module_type_ast * bool) option * module_ast option
-  | VernacDefineModule of identifier * 
+  | VernacDefineModule of lident * 
       module_binder list * (module_type_ast * bool) option * module_ast option
-  | VernacDeclareModuleType of identifier * 
+  | VernacDeclareModuleType of lident * 
       module_binder list * module_type_ast option
 
   (* Solving *)
@@ -220,30 +224,30 @@ type vernac_expr =
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
-  | VernacRequireFrom of export_flag option * specif_flag option * string
-  | VernacAddLoadPath of rec_flag * string * dir_path option
-  | VernacRemoveLoadPath of string
-  | VernacAddMLPath of rec_flag * string
-  | VernacDeclareMLModule of string list
-  | VernacChdir of string option
+  | VernacRequireFrom of export_flag option * specif_flag option * lstring
+  | VernacAddLoadPath of rec_flag * lstring * dir_path option
+  | VernacRemoveLoadPath of lstring
+  | VernacAddMLPath of rec_flag * lstring
+  | VernacDeclareMLModule of lstring list
+  | VernacChdir of lstring option
 
   (* State management *)
-  | VernacWriteState of string
-  | VernacRestoreState of string
+  | VernacWriteState of lstring
+  | VernacRestoreState of lstring
 
   (* Resetting *)
-  | VernacResetName of identifier located
+  | VernacResetName of lident
   | VernacResetInitial
   | VernacBack of int
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
-      rec_flag * (identifier located * raw_tactic_expr) list
-  | VernacHints of locality_flag * string list * hints
-  | VernacSyntacticDefinition of identifier * constr_expr * int option
-  | VernacDeclareImplicits of reference * explicitation list option
-  | VernacReserve of identifier list * constr_expr
-  | VernacSetOpacity of opacity_flag * reference list
+      rec_flag * (lident * raw_tactic_expr) list
+  | VernacHints of locality_flag * lstring list * hints
+  | VernacSyntacticDefinition of lident * constr_expr * int option
+  | VernacDeclareImplicits of lreference * explicitation list option
+  | VernacReserve of lident list * constr_expr
+  | VernacSetOpacity of opacity_flag * lreference list
   | VernacUnsetOption of Goptions.option_name
   | VernacSetOption of Goptions.option_name * option_value
   | VernacAddOption of Goptions.option_name * option_ref_value list
@@ -260,11 +264,11 @@ type vernac_expr =
 
   (* Proof management *)
   | VernacGoal of constr_expr
-  | VernacAbort of identifier located option
+  | VernacAbort of lident option
   | VernacAbortAll
   | VernacRestart
   | VernacSuspend
-  | VernacResume of identifier located option
+  | VernacResume of lident option
   | VernacUndo of int
   | VernacFocus of int option
   | VernacUnfocus