IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).

MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.

KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.


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

5 files changed, 33 insertions, 25 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 3d468d3281..c9ed58c795 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -150,7 +150,7 @@ let uniform_cond nargs lt =
 let id_of_cl  = function
   | CL_FUN -> id_of_string "FUNCLASS"
   | CL_SORT -> id_of_string "SORTCLASS"
-  | CL_CONST kn -> id_of_label (label kn)
+  | CL_CONST kn -> id_of_label (con_label kn)
   | CL_IND ind ->
       let (_,mip) = Global.lookup_inductive ind in
       mip.mind_typename
@@ -271,7 +271,7 @@ let build_id_coercion idf_opt source =
 	const_entry_type = Some typ_f;
         const_entry_opaque = false;
 	const_entry_boxed = Options.boxed_definitions()} in
-  let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+  let kn = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
   ConstRef kn
 
 let check_source = function
@@ -390,13 +390,17 @@ let defined_in_sec kn olddir =
   let _,dir,_ = repr_kn kn in
     dir = olddir
 
+let con_defined_in_sec kn olddir = 
+  let _,dir,_ = repr_con kn in
+    dir = olddir
+
 (* This moves the global path one step below *)
 let process_global olddir = function
   | VarRef _ ->
       anomaly "process_global only processes global surviving the section"
   | ConstRef kn as x ->
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
+      if con_defined_in_sec kn olddir then
+        let newkn = Lib.make_con (id_of_label (con_label kn)) in
         ConstRef newkn
       else x
   | IndRef (kn,i) as x -> 
@@ -416,8 +420,8 @@ let process_class olddir ids_to_discard x =
   match cl with 
     | CL_SECVAR _ -> x
     | CL_CONST kn -> 
-       if defined_in_sec kn olddir then
-         let newkn = Lib.make_kn (id_of_label (label kn)) in
+       if con_defined_in_sec kn olddir then
+         let newkn = Lib.make_con (id_of_label (con_label kn)) in
 	 let hyps = (Global.lookup_constant kn).const_hyps in
 	 let n = count_extra_abstractions hyps ids_to_discard in
            (CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
@@ -437,8 +441,8 @@ let process_cl sec_sp cl =
   match cl with
     | CL_SECVAR id -> cl
     | CL_CONST kn ->
-	if defined_in_sec kn sec_sp then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
+	if con_defined_in_sec kn sec_sp then
+          let newkn = Lib.make_con (id_of_label (con_label kn)) in
           CL_CONST newkn
         else 
 	  cl
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8eaab89d34..a17d446660 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -113,7 +113,7 @@ let red_constant_entry ce = function
 	  reduction_of_redexp red (Global.env()) Evd.empty body }
 
 let declare_global_definition ident ce local =
-  let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in
+  let kn = declare_constant ident (DefinitionEntry ce,IsDefinition) in
   if local = Local then
     msg_warning (pr_id ident ++ str" is declared as a global definition");
   definition_message ident;
@@ -166,7 +166,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
           str" is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
-        let (_,kn) =
+        let kn =
           declare_constant ident (ParameterEntry c, IsAssumption kind) in
         assumption_message ident;
         if local=Local & Options.is_verbose () then
@@ -215,7 +215,7 @@ let declare_one_elimination ind =
   if List.mem InType kelim then
     let elim = make_elim (new_sort_in_family InType) in
     let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in
-    let c = mkConst (snd cte) and t = constant_type (Global.env()) (snd cte) in
+    let c = mkConst cte and t = constant_type (Global.env()) cte in
     List.iter (fun (sort,suff) -> 
       let (t',c') = 
 	Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort)
@@ -514,7 +514,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
         const_entry_type = Some arrec.(i);
         const_entry_opaque = false;
         const_entry_boxed = boxed} in
-    let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+    let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
     (ConstRef kn)
   in 
   (* declare the recursive definitions *)
@@ -581,7 +581,7 @@ let build_corecursive lnameardef boxed =
         const_entry_opaque = false;
         const_entry_boxed = boxed } 
     in
-    let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+    let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
     (ConstRef kn)
   in 
   let lrefrec = Array.mapi declare namerec in
@@ -621,7 +621,7 @@ let build_scheme lnamedepindsort =
                const_entry_type = Some decltype;
                const_entry_opaque = false;
 	       const_entry_boxed = Options.boxed_definitions() } in
-    let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+    let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
     ConstRef kn :: lrecref
   in 
   let lrecref = List.fold_right2 declare listdecl lrecnames [] in
@@ -666,11 +666,11 @@ let save id const kind hook =
 	(Local, VarRef id)
     | IsLocal ->
         let k = IsDefinition in
-        let _,kn = declare_constant id (DefinitionEntry const, k) in
+        let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn)
     | IsGlobal k ->
         let k = theorem_kind_of_goal_kind k in
-        let _,kn = declare_constant id (DefinitionEntry const, k) in
+        let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   hook l r;
   Pfedit.delete_current_proof ();
@@ -707,7 +707,7 @@ let admit () =
   if k <> IsGlobal (Proof Conjecture) then
     error "Only statements declared as conjecture can be admitted";
 *)
-  let (_,kn) =
+  let kn =
     declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
   hook Global (ConstRef kn);
   Pfedit.delete_current_proof ();
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b1ba1f7480..443fd61e1a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -41,6 +41,10 @@ let recalc_kn dir kn =
   let (mp,_,l) = Names.repr_kn kn in
     Names.make_kn mp dir l
 
+let recalc_con dir con = 
+  let (mp,_,l) = Names.repr_con con in
+    Names.make_con mp dir l
+
 let rec find_var id = function
   | [] -> false
   | (x,b,_)::l -> if x = id then b=None else find_var id l
@@ -214,10 +218,10 @@ let process_object oldenv olddir full_olddir newdir
 	(* CONSTANT means never discharge (though visibility may vary) *)
  	let kind = constant_kind sp in
 	let kn = Nametab.locate_constant (qualid_of_sp sp) in
-	let lab = label kn in
+	let lab = con_label kn in
 	let cb = Environ.lookup_constant kn oldenv in
 	let imp = is_implicit_constant kn in
-	let newkn = recalc_kn newdir kn in
+	let newkn = recalc_con newdir kn in
 	let abs_vars,discharged_hyps0 =
          build_abstract_list full_olddir cb.const_hyps ids_to_discard in
         (* let's add the new discharged hypothesis to those already discharged*)
@@ -268,12 +272,12 @@ let process_object oldenv olddir full_olddir newdir
 	  let mib = Environ.lookup_mind newkn (Global.env ()) in
 	  { s_CONST = info.s_CONST;
 	    s_PARAM = mib.mind_packets.(0).mind_nparams;
-	    s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in
+	    s_PROJ = List.map (option_app (fun kn -> recalc_con newdir kn)) info.s_PROJ } in
 	((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
 
     | "OBJDEF1" -> 
 	let kn = outObjDef1 lobj in
-	let new_kn = recalc_kn newdir kn in
+	let new_kn = recalc_con newdir kn in
         ((Objdef new_kn)::ops, ids_to_discard, work_alist)
 
     | "REQUIRE" -> 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index bc037f851b..de6778291f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1110,7 +1110,7 @@ let rec reify_meta_ast vars = function
       Smetalam (loc,string_of_id id,reify_meta_ast vars body)
   | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body)
   | Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id)
-  | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a
+  | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ | ConPath _ as a -> a
   | Dynamic _ as a -> (* Hum... what to do here *) a
 
 (* For old ast syntax *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 91f5b4ad88..ee189377d7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -176,7 +176,7 @@ let declare_projections indsp coers fields =
 	        it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
               let projtyp =
                 it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
-	      let (sp,kn) =
+	      let kn =
 	        try
 		  let cie = {
 		    const_entry_body = proj;
@@ -184,9 +184,9 @@ let declare_projections indsp coers fields =
                     const_entry_opaque = false;
 		    const_entry_boxed = false } in
 		  let k = (DefinitionEntry cie,IsDefinition) in
-		  let sp = declare_internal_constant fid k in
+		  let kn = declare_internal_constant fid k in
 		  Options.if_verbose message (string_of_id fid ^" is defined");
-		  sp
+		  kn
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
 	      let refi = ConstRef kn in