From 99cdbc25a3a92545544a087ed55240c488b42fc9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 11 Jun 2014 16:55:29 +0200 Subject: Fix bug #3289 --- interp/constrintern.ml | 2 +- intf/vernacexpr.mli | 2 +- parsing/g_vernac.ml4 | 4 ++-- printing/ppvernac.ml | 2 +- tactics/rewrite.ml | 5 +++-- test-suite/bugs/closed/3289.v | 27 +++++++++++++++++++++++++++ test-suite/bugs/opened/3289.v | 21 --------------------- toplevel/classes.ml | 4 ++-- toplevel/classes.mli | 2 +- 9 files changed, 38 insertions(+), 31 deletions(-) create mode 100644 test-suite/bugs/closed/3289.v delete mode 100644 test-suite/bugs/opened/3289.v diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 475f8d396c..841a895849 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1496,7 +1496,7 @@ let internalize globalenv env allow_patvar lvar c = let cargs = sort_fields true loc fs (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), None) :: l) - in + in begin match cargs with | None -> user_err_loc (loc, "intern", str"No constructor inference.") diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 3ffaca1138..be7e59a2de 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -320,7 +320,7 @@ type vernac_expr = bool * (* abstract instance *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) - constr_expr option * (* props *) + (bool * constr_expr) option * (* props *) int option (* Priority *) | VernacContext of local_binder list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3c3caa140b..39c93e316c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -593,8 +593,8 @@ GEXTEND Gram | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] ; - props = [ ":="; "{"; r = record_declaration; "}" -> Some r | - ":="; c = lconstr -> Some c | -> None ] -> + props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | + ":="; c = lconstr -> Some (false,c) | -> None ] -> VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) | IDENT "Existing"; IDENT "Instance"; id = global; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 16759a3d83..5cad4806d4 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -728,7 +728,7 @@ let rec pr_vernac = function str":" ++ spc () ++ pr_constr cl ++ pr_priority pri ++ (match props with - | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr p + | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) | VernacContext l -> diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b4e1683eb8..aa0152d35a 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1685,7 +1685,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) - binders instance (Some (CRecord (Loc.ghost,None,fields))) + binders instance (Some (true, CRecord (Loc.ghost,None,fields))) ~global ~generalize:false None let declare_instance_refl global binders a aeq n lemma = @@ -1895,7 +1895,8 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance (Some (CRecord (Loc.ghost,None,[]))) + ignore(new_instance ~global:glob poly binders instance + (Some (true, CRecord (Loc.ghost,None,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) (** Bind to "rewrite" too *) diff --git a/test-suite/bugs/closed/3289.v b/test-suite/bugs/closed/3289.v new file mode 100644 index 0000000000..4542b015d0 --- /dev/null +++ b/test-suite/bugs/closed/3289.v @@ -0,0 +1,27 @@ +(* File reduced by coq-bug-finder from original input, then from 1829 lines to 37 lines, then from 47 lines to 18 lines *) + +Class Contr_internal (A : Type) := + BuildContr { center : A ; + contr : (forall y : A, True) }. +Class Contr A := Contr_is_contr : Contr_internal A. +Inductive Unit : Set := tt. +Instance contr_unit : Contr Unit | 0 := + let x := {| + center := tt; + contr := fun t : Unit => I + |} in x. (* success *) + +Instance contr_internal_unit' : Contr_internal Unit | 0 := + {| + center := tt; + contr := fun t : Unit => I + |}. + +Instance contr_unit' : Contr Unit | 0 := + {| + center := tt; + contr := fun t : Unit => I + |}. +(* Error: Mismatched contexts while declaring instance: + Expected: (Contr_is_contr : Contr_internal _UNBOUND_REL_1) + Found: tt (fun t : Unit => I) *) diff --git a/test-suite/bugs/opened/3289.v b/test-suite/bugs/opened/3289.v deleted file mode 100644 index 63453c5b81..0000000000 --- a/test-suite/bugs/opened/3289.v +++ /dev/null @@ -1,21 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 1829 lines to 37 lines, then from 47 lines to 18 lines *) - -Class Contr_internal (A : Type) := - BuildContr { center : A ; - contr : (forall y : A, True) }. -Class Contr A := Contr_is_contr : Contr_internal A. -Inductive Unit : Set := tt. -Instance contr_unit : Contr Unit | 0 := - let x := {| - center := tt; - contr := fun t : Unit => I - |} in x. (* success *) - -Fail Instance contr_unit' : Contr Unit | 0 := - {| - center := tt; - contr := fun t : Unit => I - |}. -(* Error: Mismatched contexts while declaring instance: - Expected: (Contr_is_contr : Contr_internal _UNBOUND_REL_1) - Found: tt (fun t : Unit => I) *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 56f9cb5647..07f4354b52 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -187,11 +187,11 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro else ( let props = match props with - | Some (CRecord (loc, _, fs)) -> + | Some (true, CRecord (loc, _, fs)) -> if List.length fs > List.length k.cl_props then mismatched_props env' (List.map snd fs) k.cl_props; Some (Inl fs) - | Some t -> Some (Inr t) + | Some (_, t) -> Some (Inr t) | None -> if Flags.is_program_mode () then Some (Inl []) else None diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 4dd62ba9fc..fb3da98ad3 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -48,7 +48,7 @@ val new_instance : Decl_kinds.polymorphic -> local_binder list -> typeclass_constraint -> - constr_expr option -> + (bool * constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(Globnames.global_reference -> unit) -> -- cgit v1.2.3