Intgration uniforme de coercions dans les dclarations (Variable and co) et retouche des Record

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

6 files changed, 31 insertions, 43 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 234910af0..c6a038c3b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -83,7 +83,7 @@ let declare_definition red_option ident (local,n) c typopt =
     | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
 	  let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type) in
-          let sp = declare_variable ident (Lib.cwd(), c, n) in
+          let _ = declare_variable ident (Lib.cwd(), c, n) in
 	  if_verbose message ((string_of_id ident) ^ " is defined");
           if Pfedit.refining () then 
             msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ 
@@ -110,22 +110,25 @@ let declare_assumption ident n c =
   let c = interp_type Evd.empty (Global.env()) c in
   match n with
     | NeverDischarge ->
-	let _ = declare_constant ident (ParameterEntry c, NeverDischarge) in
-	assumption_message ident
+	let r = declare_constant ident (ParameterEntry c, NeverDischarge) in
+	assumption_message ident;
+	ConstRef r
     | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
-          let _ = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in
+          let r = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in
 	  assumption_message ident;
           if is_verbose () & Pfedit.refining () then 
             msgerrnl (str"Warning: Variable " ++ pr_id ident ++ 
-                      str" is not visible from current goals")
+                      str" is not visible from current goals");
+	  VarRef ident
         end
 	else
-	  let _ = declare_constant ident (ParameterEntry c, NeverDischarge) in
+	  let r = declare_constant ident (ParameterEntry c, NeverDischarge) in
 	  assumption_message ident;
 	  if_verbose
 	    msg_warning (pr_id ident ++ str" is declared as a parameter" ++
                str" because it is at a global level");
+	  ConstRef r
     | NotDeclare ->
       anomalylabstrm "Command.hypothesis_def_var"
         (str "Strength NotDeclare not for Variable, only for Let")
@@ -220,7 +223,7 @@ let eq_la (id,ast) (id',ast') = id = id' & alpha_eq(ast,ast')
 
 let extract_coe lc =
   List.fold_right
-    (fun (id,addcoe,t) (l1,l2) ->
+    (fun (addcoe,(id,t)) (l1,l2) ->
       ((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[])
 
 let extract_coe_la_lc = function
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 474fe9202..ea6c97e0e 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -21,32 +21,12 @@ open Library
    functions of [Declare]; they return an absolute reference to the
    defined object *)
 
-(*i
-val constant_entry_of_com :
-  Coqast.t * Coqast.t option * bool -> Safe_typing.constant_entry
-
-val declare_global_definition :
-  Names.identifier ->
-  Safe_typing.constant_entry ->
-  Declare.strength -> bool -> Nametab.global_reference
-
-val definition_body : identifier -> bool * strength -> 
-  Coqast.t -> Coqast.t option -> global_reference
-i*)
-
 val declare_definition : Tacred.red_expr option -> identifier
   -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference
 
 val syntax_definition : identifier -> Coqast.t -> unit
 
-(*i
-val hypothesis_def_var : bool -> identifier -> strength -> Coqast.t
-  -> global_reference
-
-val parameter_def_var : identifier -> Coqast.t -> constant
-i*)
-
-val declare_assumption : identifier -> strength -> Coqast.t -> unit
+val declare_assumption : identifier -> strength -> Coqast.t -> global_reference
 
 val build_mutual : Vernacexpr.inductive_expr list -> bool -> unit
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c7907b167..10b9c42da 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -209,7 +209,7 @@ 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 = List.length ps in
   let idps = List.map fst ps in
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 1419b9c3c..90b40020e 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -12,6 +12,7 @@
 open Names
 open Term
 open Sign
+open Vernacexpr
 (*i*)
 
 (* [declare_projections ref coers params fields] declare projections of
@@ -22,5 +23,5 @@ val declare_projections :
   inductive -> bool list -> rel_context -> constant option list
 
 val definition_structure :
-  bool * identifier * (identifier * Genarg.constr_ast) list *
-  (bool * Vernacexpr.local_decl_expr) list * identifier * sorts -> unit
+  identifier with_coercion * (identifier * Genarg.constr_ast) list *
+  (local_decl_expr with_coercion) list * identifier * sorts -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8d8de77b9..9c11ae7cb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -307,7 +307,10 @@ let vernac_exact_proof c =
 
 let vernac_assumption kind l =
   let stre = interp_assumption kind in
-  List.iter (fun (id,c) -> declare_assumption id stre c) l
+  List.iter
+    (fun (is_coe,(id,c)) ->
+      let r = declare_assumption id stre c in
+      if is_coe then Class.try_add_new_coercion r stre) l
 
 let vernac_inductive f indl = build_mutual indl f
 
@@ -321,12 +324,12 @@ let vernac_scheme = build_scheme
 (**********************)
 (* Gallina extensions *)
 
-let vernac_record iscoe struc binders sort nameopt cfs =
+let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
-    | None -> add_prefix "Build_" struc
+    | None -> add_prefix "Build_" (snd struc)
     | Some id -> id in
   let s = Astterm.interp_sort sort in
-  Record.definition_structure (iscoe,struc,binders,cfs,const,s)
+  Record.definition_structure (struc,binders,cfs,const,s)
 
   (* Sections *)
 
@@ -876,7 +879,7 @@ let interp c = match c with
   | VernacScheme l -> vernac_scheme l
 
   (* Gallina extensions *)
-  | VernacRecord (coe,id,bl,s,idopt,fs) -> vernac_record coe id bl s idopt fs
+  | VernacRecord (id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
   | VernacBeginSection id -> vernac_begin_section id
   | VernacEndSection id -> vernac_end_section id
   | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 365192599..f1bd6ed52 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -140,12 +140,13 @@ type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
 
 type sort_expr = t
 
-type simple_binders = identifier * constr_ast
-type constructor_expr = identifier * coercion_flag * constr_ast
+type simple_binder = identifier * constr_ast
+type 'a with_coercion = coercion_flag * 'a
+type constructor_expr = simple_binder with_coercion
 type inductive_expr =
-    identifier *  simple_binders list * constr_ast * constructor_expr list
+    identifier *  simple_binder list * constr_ast * constructor_expr list
 type fixpoint_expr =
-    identifier * simple_binders list * constr_ast * constr_ast
+    identifier * simple_binder list * constr_ast * constr_ast
 type cofixpoint_expr =
     identifier * constr_ast * constr_ast
 
@@ -180,15 +181,15 @@ type vernac_expr =
       constr_ast * bool * Proof_type.declaration_hook
   | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
   | VernacExactProof of constr_ast
-  | VernacAssumption of assumption_kind * simple_binders list
+  | VernacAssumption of assumption_kind * simple_binder with_coercion list
   | VernacInductive of inductive_flag * inductive_expr list
   | VernacFixpoint of fixpoint_expr list
   | VernacCoFixpoint of cofixpoint_expr list
   | VernacScheme of (identifier * bool * qualid located * sort_expr) list
 
   (* Gallina extensions *)
-  | VernacRecord of coercion_flag * identifier * simple_binders list
-      * sort_expr * identifier option * (coercion_flag * local_decl_expr) list
+  | VernacRecord of identifier with_coercion * simple_binder list
+      * sort_expr * identifier option * local_decl_expr with_coercion list
   | VernacBeginSection of identifier
   | VernacEndSection of identifier
   | VernacRequire of