diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3289.v (renamed from test-suite/bugs/opened/3289.v) | 8 | ||||
| -rw-r--r-- | toplevel/classes.ml | 4 | ||||
| -rw-r--r-- | toplevel/classes.mli | 2 |
8 files changed, 18 insertions, 11 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 475f8d396..841a89584 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 3ffaca113..be7e59a2d 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 3c3caa140..39c93e316 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 16759a3d8..5cad4806d 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 b4e1683eb..aa0152d35 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/opened/3289.v b/test-suite/bugs/closed/3289.v index 63453c5b8..4542b015d 100644 --- a/test-suite/bugs/opened/3289.v +++ b/test-suite/bugs/closed/3289.v @@ -11,7 +11,13 @@ Instance contr_unit : Contr Unit | 0 := contr := fun t : Unit => I |} in x. (* success *) -Fail Instance contr_unit' : Contr Unit | 0 := +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 diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 56f9cb564..07f4354b5 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 4dd62ba9f..fb3da98ad 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) -> |