diff options
| -rw-r--r-- | CHANGES.md | 2 | ||||
| -rw-r--r-- | plugins/syntax/g_numeral.mlg | 5 | ||||
| -rw-r--r-- | plugins/syntax/plugin_base.dune | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 18 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10025.v | 39 | ||||
| -rw-r--r-- | theories/Structures/EqualitiesFacts.v | 11 |
6 files changed, 66 insertions, 11 deletions
diff --git a/CHANGES.md b/CHANGES.md index 3c8070d585..5ca16ae1fe 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -45,6 +45,8 @@ Unreleased changes **Standard library** +- Added Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull + **Infrastructure and dependencies** diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index baa4ae0306..0f0f3953da 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -16,18 +16,17 @@ open Notation open Numeral open Pp open Names -open Ltac_plugin open Stdarg open Pcoq.Prim -let pr_numnot_option _ _ _ = function +let pr_numnot_option = function | Nop -> mt () | Warning n -> str "(warning after " ++ str n ++ str ")" | Abstract n -> str "(abstract after " ++ str n ++ str ")" } -ARGUMENT EXTEND numnotoption +VERNAC ARGUMENT EXTEND numnotoption PRINTED BY { pr_numnot_option } | [ ] -> { Nop } | [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft } diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune index aac46338ea..7a23581768 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/plugin_base.dune @@ -3,7 +3,7 @@ (public_name coq.plugins.numeral_notation) (synopsis "Coq numeral notation plugin") (modules g_numeral numeral) - (libraries coq.plugins.ltac)) + (libraries coq.vernac)) (library (name string_notation_plugin) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 16bede0d1b..35b3b38298 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2863,17 +2863,21 @@ let generalize_dep ?(with_let=false) c = | _ -> tothin in let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in - let body = - if with_let then - match EConstr.kind sigma c with - | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value - | _ -> None - else None + let is_var, body = match EConstr.kind sigma c with + | Var id -> + let body = NamedDecl.get_value (pf_get_hyp id gl) in + let is_var = Option.is_empty body && not (List.mem id init_ids) in + if with_let then is_var, body else is_var, None + | _ -> false, None in let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in (* Check that the generalization is indeed well-typed *) - let (evd, _) = Typing.type_of env evd cl'' in + let evd = + (* No need to retype for variables, term is statically well-typed *) + if is_var then evd + else fst (Typing.type_of env evd cl'') + in let args = Context.Named.to_instance mkVar to_quantify_rev in tclTHENLIST [ Proofview.Unsafe.tclEVARS evd; diff --git a/test-suite/bugs/closed/bug_10025.v b/test-suite/bugs/closed/bug_10025.v new file mode 100644 index 0000000000..1effc771b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_10025.v @@ -0,0 +1,39 @@ +Require Import Program. + +Axiom I : Type. + +Inductive S : Type := NT : I -> S. + +Axiom F : S -> Type. + +Axiom G : forall (s : S), F s -> Type. + +Section S. + +Variable init : I. +Variable my_s : F (NT init). + +Inductive foo : forall (s: S) (hole_sem: F s), Type := +| Foo : foo (NT init) my_s. + +Goal forall + (n : I) (s : F (NT n)) (ptz : foo (NT n) s) (pt : G (NT n) s) (x : unit), +match + match x with tt => tt end +with +| tt => + match + match ptz in foo x s return (forall _ : G x s, unit) with + | Foo => fun _ : G (NT init) my_s => tt + end pt + with + | tt => False + end +end. +Proof. +dependent destruction ptz. +(* Check well-typedness of goal *) +match goal with [ |- ?P ] => let t := type of P in idtac end. +Abort. + +End S. diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index c738b57f44..0f63855b55 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -212,3 +212,14 @@ Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Defined. End PairUsualDecidableType. + +(** And also for pairs of UsualDecidableTypeFull *) + +Module PairUsualDecidableTypeFull (D1 D2:UsualDecidableTypeFull) + <: UsualDecidableTypeFull. + + Module M := PairUsualDecidableType D1 D2. + Include Backport_DT (M). + Include HasEqDec2Bool. + +End PairUsualDecidableTypeFull. |