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

4 files changed, 13 insertions, 38 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
index fc15a88f7b..fc99daab68 100644
--- a/test-suite/bugs/closed/HoTT_coq_098.v
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -37,35 +37,10 @@ Module success.
   Admitted.
 End success.
 
-Module failure.
+Module success2.
   Section SpecializedFunctor.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-
-    Polymorphic Record SpecializedFunctor
-      := {
-          ObjectOf' : objC -> objD;
-          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
-        }.
-  End SpecializedFunctor.
-
-  Set Printing Universes.
-  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
-  (* Toplevel input, characters 73-94:
-Error:
-The term "GraphIndexingCategory (* Top.563 *)" has type
- "SpecializedCategory (* Top.563 Set *) GraphIndex"
-while it is expected to have type
- "SpecializedCategory (* Top.550 Top.551 *) ?7"
-(Universe inconsistency: Cannot enforce Set = Top.551)). *)
-  admit.
-  Defined.
-End failure.
-
-Module polycontext.
-  Section SpecializedFunctor.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
+    Polymorphic Context `(C : @SpecializedCategory objC).
+    Polymorphic Context `(D : @SpecializedCategory objD).
 
     Polymorphic Record SpecializedFunctor
       := {
@@ -85,4 +60,4 @@ while it is expected to have type
 (Universe inconsistency: Cannot enforce Set = Top.551)). *)
   admit.
   Defined.
-End polycontext.
+End success2.
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"