Add [Polymorphic] flag for defs

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

6 files changed, 21 insertions, 17 deletions

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index fbdaa8d3b1..7faf780330 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -113,7 +113,7 @@ let dump_constraint ty ((loc, n), _, _) =
 let dump_variable lid = ()
 
 let vernac_assumption env isevars kind l nl =
-  let global = fst kind = Global in
+  let global = pi1 kind = Global in
     List.iter (fun (is_coe,(idl,c)) ->
       if Dumpglob.dump () then
 	List.iter (fun lid ->
@@ -137,7 +137,8 @@ let subtac (loc, command) =
       Dumpglob.dump_definition lid false "def";
       (match expr with
       | ProveBody (bl, t) ->
-	  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
+	  start_proof_and_print env isevars (Some lid) 
+	    (pi1 defkind, pi2 defkind, DefinitionBody Definition) (bl,t)
 	    (fun _ _ -> ())
       | DefineBody (bl, _, c, tycon) ->
 	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
@@ -148,7 +149,7 @@ let subtac (loc, command) =
       let _ = trace (str "Building fixpoint") in
 	ignore(Subtac_command.build_recursive l)
 
-  | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
+  | VernacStartTheoremProof (thkind, p, [Some id, (bl,t,guard)], lettop, hook) ->
       if guard <> None then 
         error "Do not support building theorems as a fixpoint.";
       Dumpglob.dump_definition id false "prf";
@@ -160,12 +161,12 @@ let subtac (loc, command) =
 	errorlabstrm "Subtac_command.StartProof"
 	  (str "Proof editing mode not supported in module types");
       check_fresh id;
-      start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
+      start_proof_and_print env isevars (Some id) (Global, p, Proof thkind) (bl,t) hook
 
   | VernacAssumption (stre,nl,l) ->
       vernac_assumption env isevars stre l nl
 
-  | VernacInstance (abst, glob, sup, is, props, pri) ->
+  | VernacInstance (abst, glob, poly, sup, is, props, pri) ->
       dump_constraint "inst" is;
       if abst then
 	error "Declare Instance not supported here.";
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 05e634c58b..0a3da4d0c8 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -180,4 +180,4 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   in
   let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
   let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in
-    id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls
+    id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index f02e83ad1a..5c7f7b5ec0 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -327,6 +327,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	let ce =
 	  { const_entry_body = Evarutil.nf_evar !isevars body;
 	    const_entry_type = Some ty;
+	    const_entry_polymorphic = false;
 	    const_entry_opaque = false }
 	in 
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 76cc7644d6..874cce85c9 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -231,10 +231,11 @@ let subst_body expand prg =
 
 let declare_definition prg =
   let body, typ = subst_body true prg in
-  let (local, kind) = prg.prg_kind in
+  let (local, poly, kind) = prg.prg_kind in
   let ce =
     { const_entry_body = body;
       const_entry_type = Some typ;
+      const_entry_polymorphic = poly;
       const_entry_opaque = false }
   in
     (Command.get_declare_definition_hook ()) ce;
@@ -253,7 +254,7 @@ let declare_definition prg =
     | (Global|Local) ->
 	let c =
 	  Declare.declare_constant
-	    prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind))
+	    prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
 	in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
@@ -301,7 +302,7 @@ let declare_mutual_definition l =
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let (local,kind) = first.prg_kind in
+  let (local,poly,kind) = first.prg_kind in
   let fixnames = first.prg_deps in
   let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
@@ -334,6 +335,7 @@ let declare_obligation prg obl body =
       let ce = 
 	{ const_entry_body = body;
 	  const_entry_type = Some ty;
+	  const_entry_polymorphic = false;
 	  const_entry_opaque = opaque }
       in
       let constant = Declare.declare_constant obl.obl_name
@@ -602,7 +604,7 @@ let show_term n =
 	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
@@ -620,7 +622,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
     ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 7fba23dc23..6487a14b7f 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -218,13 +218,13 @@ let non_instanciated_map env evd evm =
     Evd.empty (Evarutil.non_instantiated evm)
 
 let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
 let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
-let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma
 
 let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
-let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
+let goal_fix_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
 
 open Tactics
 open Tacticals
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 2753a2522c..d2c3fd0c8c 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -95,11 +95,11 @@ val string_of_hole_kind : hole_kind -> string
 val evars_of_term : evar_map -> evar_map -> constr -> evar_map
 val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map
 val global_kind : logical_kind
-val goal_kind : locality * goal_object_kind
+val goal_kind : locality * polymorphic * goal_object_kind
 val global_proof_kind : logical_kind
-val goal_proof_kind : locality * goal_object_kind
+val goal_proof_kind : locality * polymorphic * goal_object_kind
 val global_fix_kind : logical_kind
-val goal_fix_kind : locality * goal_object_kind
+val goal_fix_kind : locality * polymorphic * goal_object_kind
 
 val mkSubset : name -> constr -> constr -> constr
 val mkProj1 : constr -> constr -> constr -> constr