Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.

3 files changed, 9 insertions, 9 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d888d6ffac..e8e3ef27dc 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -324,7 +324,7 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
-let context l =
+let context poly l =
   let env = Global.env() in
   let evars = ref Evd.empty in
   let _, ((env', fullctx), impls) = interp_context_evars evars env l in
@@ -341,12 +341,12 @@ let context l =
   let fn status (id, b, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       let uctx = Univ.ContextSet.to_context uctx in	
-      let decl = (ParameterEntry (None,false,(t,uctx),None), IsAssumption Logical) in
+      let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in
 	match class_of_constr t with
 	| Some (rels, ((tc,_), args) as _cl) ->
 	    add_instance (Typeclasses.new_instance tc None false (*FIXME*)
-			  (Flags.use_polymorphic_flag ()) (ConstRef cst));
+			    poly (ConstRef cst));
             status
 	    (* declare_subclasses (ConstRef cst) cl *)
 	| None -> status
@@ -356,7 +356,7 @@ let context l =
       | _ -> false
       in
       let impl = List.exists test impls in
-      let decl = (Discharge, (Flags.use_polymorphic_flag ()), Definitional) in
+      let decl = (Discharge, poly, Definitional) in
       let nstatus =
         pi3 (Command.declare_assumption false decl (t, uctx) [] impl
           Vernacexpr.NoInline (Loc.ghost, id))
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index fb3da98ad3..489f2aa5f7 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -67,7 +67,7 @@ val id_of_class : typeclass -> Id.t
 
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
-val context : local_binder list -> bool
+val context : Decl_kinds.polymorphic -> local_binder list -> bool
 
 (** Forward ref for refine *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 27b53579f5..2e97b74d66 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -794,8 +794,8 @@ let vernac_instance abst locality poly sup inst props pri =
   Dumpglob.dump_constraint inst false "inst";
   ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
 
-let vernac_context l =
-  if not (Classes.context l) then Pp.feedback Interface.AddedAxiom
+let vernac_context poly l =
+  if not (Classes.context poly l) then Pp.feedback Interface.AddedAxiom
 
 let vernac_declare_instances locality ids pri =
   let glob = not (make_section_locality locality) in
@@ -1746,7 +1746,7 @@ let interp ?proof locality poly c =
   (* Type classes *)
   | VernacInstance (abst, sup, inst, props, pri) ->
       vernac_instance abst locality poly sup inst props pri
-  | VernacContext sup -> vernac_context sup
+  | VernacContext sup -> vernac_context poly sup
   | VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri
   | VernacDeclareClass id -> vernac_declare_class id
 
@@ -1872,7 +1872,7 @@ let check_vernac_supports_polymorphism c p =
     | VernacStartTheoremProof _
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
-    | VernacHints _
+    | VernacHints _ | VernacContext _
     | VernacExtend _ ) -> ()
   | Some _, _ -> Errors.error "This command does not support Polymorphism"