aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/term_typing.ml46
-rw-r--r--plugins/extraction/Extraction.v0
-rw-r--r--plugins/extraction/vo.itarget1
-rw-r--r--plugins/funind/FunInd.v0
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/vo.itarget1
-rw-r--r--tactics/tactics.ml2
-rw-r--r--test-suite/bugs/closed/5372.v7
-rw-r--r--theories/Lists/List.v4
-rw-r--r--theories/QArith/Qround.v2
10 files changed, 36 insertions, 30 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 22b7eebcb..569a58378 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,24 +24,6 @@ open Typeops
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-let constrain_type env j poly subst = function
- | `None ->
- if not poly then (* Old-style polymorphism *)
- make_polymorphic_if_constant_for_ind env j
- else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
- | `Some t ->
- let tj = infer_type env t in
- let _ = judge_of_cast env j DEFAULTcast tj in
- assert (eq_constr t tj.utj_val);
- RegularArity (Vars.subst_univs_level_constr subst t)
- | `SomeWJ (t, tj) ->
- let tj = infer_type env t in
- let _ = judge_of_cast env j DEFAULTcast tj in
- assert (eq_constr t tj.utj_val);
- RegularArity (Vars.subst_univs_level_constr subst t)
-
-let map_option_typ = function None -> `None | Some x -> `Some x
-
(* Insertion of constants and parameters in environment. *)
let mk_pure_proof c = (c, Univ.ContextSet.empty), []
@@ -183,6 +165,10 @@ let infer_declaration ~trust env kn dcl =
let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
Undef nl, RegularArity t, None, poly, univs, false, ctx
+ (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
+ so we delay the typing and hash consing of its body.
+ Remark: when the universe quantification is given explicitly, we could
+ delay even in the polymorphic case. *)
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
const_entry_polymorphic = false} as c) ->
@@ -194,15 +180,16 @@ let infer_declaration ~trust env kn dcl =
let body, uctx, signatures =
inline_side_effects env body uctx side_eff in
let valid_signatures = check_signatures trust signatures in
- let env' = push_context_set uctx env in
+ let env = push_context_set uctx env in
let j =
- let body,env',ectx = skip_trusted_seff valid_signatures body env' in
- let j = infer env' body in
+ let body,env,ectx = skip_trusted_seff valid_signatures body env in
+ let j = infer env body in
unzip ectx j in
let j = hcons_j j in
let subst = Univ.LMap.empty in
- let _typ = constrain_type env' j c.const_entry_polymorphic subst
- (`SomeWJ (typ,tyj)) in
+ let _ = judge_of_cast env j DEFAULTcast tyj in
+ assert (eq_constr typ tyj.utj_val);
+ let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in
feedback_completion_typecheck feedback_id;
j.uj_val, uctx) in
let def = OpaqueDef (Opaqueproof.create proofterm) in
@@ -210,6 +197,7 @@ let infer_declaration ~trust env kn dcl =
c.const_entry_universes,
c.const_entry_inline_code, c.const_entry_secctx
+ (** Other definitions have to be processed immediately. *)
| DefinitionEntry c ->
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
@@ -222,7 +210,17 @@ let infer_declaration ~trust env kn dcl =
let usubst, univs =
Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in
let j = infer env body in
- let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+ let typ = match typ with
+ | None ->
+ if not c.const_entry_polymorphic then (* Old-style polymorphism *)
+ make_polymorphic_if_constant_for_ind env j
+ else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
+ | Some t ->
+ let tj = infer_type env t in
+ let _ = judge_of_cast env j DEFAULTcast tj in
+ assert (eq_constr t tj.utj_val);
+ RegularArity (Vars.subst_univs_level_constr usubst t)
+ in
let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
let def =
if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/plugins/extraction/Extraction.v
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 9c30c5eb3..3563f71df 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,3 +1,4 @@
+Extraction.vo
ExtrHaskellBasic.vo
ExtrHaskellNatNum.vo
ExtrHaskellNatInt.vo
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/plugins/funind/FunInd.v
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 527f4f0b1..3199474dd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1217,7 +1217,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let mk_fixes : tactic =
let pre_info,infos = list_chop fun_num infos in
match pre_info,infos with
- | [],[] -> tclIDTAC
+ | _,[] -> tclIDTAC
| _, this_fix_info::others_infos ->
let other_fix_infos =
List.map
@@ -1233,7 +1233,6 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
else
Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos 0)
- | _ -> anomaly (Pp.str "Not a valid information")
in
let first_tac : tactic = (* every operations until fix creations *)
tclTHENSEQ
diff --git a/plugins/funind/vo.itarget b/plugins/funind/vo.itarget
index 33c968302..a17a5ec12 100644
--- a/plugins/funind/vo.itarget
+++ b/plugins/funind/vo.itarget
@@ -1 +1,2 @@
+FunInd.vo
Recdef.vo
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 84d09d833..8a78037ce 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3023,7 +3023,7 @@ let warn_unused_intro_pattern =
(fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
let check_unused_names names =
- if not (List.is_empty names) && Flags.is_verbose () then
+ if not (List.is_empty names) then
warn_unused_intro_pattern names
let intropattern_of_name gl avoid = function
diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
new file mode 100644
index 000000000..2dc78d4c7
--- /dev/null
+++ b/test-suite/bugs/closed/5372.v
@@ -0,0 +1,7 @@
+(* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Function odd (n:nat) :=
+ match n with
+ | 0 => false
+ | S n => true
+ end
+with even (n:nat) := false.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 30f1dec22..1aece3f60 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -419,7 +419,7 @@ Section Elts.
Proof.
unfold lt; induction n as [| n hn]; simpl.
- destruct l; simpl; [ inversion 2 | auto ].
- - destruct l as [| a l hl]; simpl.
+ - destruct l; simpl.
* inversion 2.
* intros d ie; right; apply hn; auto with arith.
Qed.
@@ -1280,7 +1280,7 @@ End Fold_Right_Recursor.
partition l = ([], []) <-> l = [].
Proof.
split.
- - destruct l as [|a l' _].
+ - destruct l as [|a l'].
* intuition.
* simpl. destruct (f a), (partition l'); now intros [= -> ->].
- now intros ->.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 0ed6d557c..e94ef408d 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -141,7 +141,7 @@ Qed.
Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).
Proof.
unfold Qfloor. intros. simpl.
- destruct m as [?|?|p]; simpl.
+ destruct m as [ | | p]; simpl.
now rewrite Zdiv_0_r, Z.mul_0_r.
now rewrite Z.mul_1_r.
rewrite <- Z.opp_eq_mul_m1.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 17:11:55 +0000