diff options
26 files changed, 331 insertions, 215 deletions
diff --git a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh new file mode 100644 index 0000000000..95f0de2bd3 --- /dev/null +++ b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "13386" ] || [ "$CI_BRANCH" = "master+fix9971-primproj-canonical-structure-on-evar-type" ]; then + + unicoq_CI_REF=master+adapting-coq-pr13386 + unicoq_CI_GITURL=https://github.com/herbelin/unicoq + + elpi_CI_REF=coq-master+adapting-coq-pr13386 + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst new file mode 100644 index 0000000000..4bd214d7be --- /dev/null +++ b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst @@ -0,0 +1,6 @@ +- **Fixed:** + issue when two expressions involving different projections and one is + primitive need to be unified + (`#13386 <https://github.com/coq/coq/pull/13386>`_, + fixes `#9971 <https://github.com/coq/coq/issues/9971>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst new file mode 100644 index 0000000000..bc67fd025a --- /dev/null +++ b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst @@ -0,0 +1,6 @@ +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 <https://github.com/coq/coq/pull/13236>`_, + fixes `#13235 <https://github.com/coq/coq/issues/13235>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst index a51f96d0a2..f37fbfe52b 100644 --- a/doc/changelog/04-tactics/13381-bfs_eauto.rst +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -1,6 +1,6 @@ - **Deprecated:** Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``. - Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``; - replacement TBD. + Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``. + (Use ``bfs eauto`` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) (`#13381 <https://github.com/coq/coq/pull/13381>`_, by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13403-occs_nums_nat.rst b/doc/changelog/04-tactics/13403-occs_nums_nat.rst new file mode 100644 index 0000000000..5dfa90a267 --- /dev/null +++ b/doc/changelog/04-tactics/13403-occs_nums_nat.rst @@ -0,0 +1,7 @@ +- **Removed:** + :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` + no longer allow negative values. A "-" before the + list (for set complement) is still supported. Ex: "at -1 -2" + is no longer supported but "at -1 2" is. + (`#13403 <https://github.com/coq/coq/pull/13403>`_, + by Jim Fehrle). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 4d59fc0513..24fa71059c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -147,7 +147,7 @@ Specification language, type inference This makes typeclasses with declared modes more robust with respect to the order of resolution. (`#10858 <https://github.com/coq/coq/pull/10858>`_, - fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). + fixes `#9058 <https://github.com/coq/coq/issues/9058>`_, by Matthieu Sozeau). - **Added:** Warn when manual implicit arguments are used in unexpected positions of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..5283f60b11 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -274,9 +274,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. exn:: Too few occurrences. :undocumented: - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences - This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + In the presence of :n:`with`, this applies :tacn:`change` to the + occurrences specified by :n:`@goal_occurrences`. In the + absence of :n:`with`, :n:`@goal_occurrences` is expected to + only list hypotheses (and optionally the conclusion) without + specifying occurrences (i.e. no :n:`at` clause). .. tacv:: now_show @term @@ -320,7 +324,7 @@ Performing computations ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } + | - {+ {| @natural | @ident } } int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4c1956d172..816acba4c1 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1939,11 +1939,6 @@ tac2rec_fields: [ | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 ] -(* todo: weird productions, ints only after an initial "-"??: - occs_nums: [ - | LIST1 [ natural | ident ] - | "-" [ natural | ident ] LIST0 int_or_var -*) ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) | REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index b5d57f92e9..03a20d621b 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -480,6 +480,7 @@ opt_hintbases: [ command: [ | "Goal" lconstr | "Proof" +| "Proof" "using" G_vernac.section_subset_expr | "Proof" "Mode" string | "Proof" lconstr | "Abort" @@ -604,7 +605,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 reference | "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] -| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] +| "Proof" "using" G_vernac.section_subset_expr "with" Pltac.tactic | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic | "Print" "Ltac" reference | "Locate" "Ltac" reference @@ -2328,7 +2329,7 @@ conversion: [ occs_nums: [ | LIST1 nat_or_var -| "-" nat_or_var LIST0 int_or_var +| "-" LIST1 nat_or_var ] occs: [ @@ -2538,6 +2539,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index c9d70a88fc..0209cf762a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -653,7 +653,7 @@ ref_or_pattern_occ: [ occs_nums: [ | LIST1 [ natural | ident ] -| "-" [ natural | ident ] LIST0 int_or_var +| "-" LIST1 [ natural | ident ] ] int_or_var: [ @@ -953,6 +953,7 @@ command: [ | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) | "Show" "Extraction" (* extraction plugin *) | "Proof" +| "Proof" "using" section_var_expr | "Proof" "Mode" string | "Proof" term | "Abort" OPT [ "All" | ident ] @@ -1033,7 +1034,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural | "Proof" "with" ltac_expr OPT [ "using" section_var_expr ] -| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ] +| "Proof" "using" section_var_expr "with" ltac_expr | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid @@ -1969,6 +1970,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern ] eqn_ipat: [ diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b86ad7175a..c7ed066f7e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -534,15 +534,19 @@ let intern_generalized_binder intern_type ntnvars in let na = match na with | Anonymous -> - let name = - let id = - match ty with - | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> - qualid_basename qid - | _ -> default_non_dependent_ident - in Implicit_quantifiers.make_fresh ids' (Global.env ()) id - in Name name - | _ -> na in + let id = + match ty with + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> default_non_dependent_ident + in + let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in + let id = + Implicit_quantifiers.make_fresh ids' (Global.env ()) id + in + Name id + | _ -> na + in let impls = impls_type_list 1 ty' in (push_name_env ntnvars impls env' (make ?loc na), (make ?loc (na,b',ty')) :: List.rev bl) diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 236de65462..072206c39c 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -234,9 +234,7 @@ GRAMMAR EXTEND Gram ; occs_nums: [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl } - | "-"; n = nat_or_var; nl = LIST0 int_or_var -> - (* have used int_or_var instead of nat_or_var for compatibility *) - { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ] + | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ] ; occs: [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ] @@ -379,9 +377,11 @@ GRAMMAR EXTEND Gram { {onhyps=None; concl_occs=occs} } | "*"; "|-"; occs=concl_occ -> { {onhyps=None; concl_occs=occs} } - | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> + | "|-"; occs=concl_occ -> + { {onhyps=Some []; concl_occs=occs} } + | hl = LIST1 hypident_occ SEP ","; "|-"; occs=concl_occ -> { {onhyps=Some hl; concl_occs=occs} } - | hl=LIST0 hypident_occ SEP"," -> + | hl = LIST1 hypident_occ SEP "," -> { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ] ; clause_dft_concl: diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 9c75175889..292fbefb84 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -71,7 +71,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") + CErrors.user_err ~hdr:"lookup_map" (str"Map "++qs map++str"not found") let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in @@ -135,15 +135,11 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" (****************************************************************************) -let ic c = - let env = Global.env() in - let sigma = Evd.from_env env in +let ic env sigma c = let c, uctx = Constrintern.interp_constr env sigma c in (Evd.from_ctx uctx, c) -let ic_unsafe c = (*FIXME remove *) - let env = Global.env() in - let sigma = Evd.from_env env in +let ic_unsafe env sigma c = (*FIXME remove *) fst (Constrintern.interp_constr env sigma c) let decl_constant name univs c = @@ -170,8 +166,8 @@ let dummy_goal env sigma = Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in {Evd.it = gl; Evd.sigma = sigma} -let constr_of evd v = match Value.to_constr v with - | Some c -> EConstr.to_constr evd c +let constr_of sigma v = match Value.to_constr v with + | Some c -> EConstr.to_constr sigma c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -189,7 +185,7 @@ let get_res = Tacenv.register_ml_tactic name [| tac |]; entry -let exec_tactic env evd n f args = +let exec_tactic env sigma n f args = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in let x = Reference (ArgVar CAst.(make id)) in @@ -203,11 +199,11 @@ let exec_tactic env evd n f args = let get_res = TacML (CAst.make (get_res, [TacGeneric (None, n)])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (* Evaluate the whole result *) - let gl = dummy_goal env evd in + let gl = dummy_goal env sigma in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd = Evd.minimize_universes gls.Evd.sigma in - let nf c = constr_of evd c in - Array.map nf !tactic_res, Evd.universe_context_set evd + let sigma = Evd.minimize_universes gls.Evd.sigma in + let nf c = constr_of sigma c in + Array.map nf !tactic_res, Evd.universe_context_set sigma let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) @@ -222,10 +218,9 @@ let coq_nil = gen_reference "core.list.nil" let lapp f args = mkApp(Lazy.force f,args) -let plapp evdref f args = - let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in - evdref := evd; - mkApp(fc,args) +let plapp sigma f args = + let sigma, fc = Evarutil.new_global sigma (Lazy.force f) in + sigma, mkApp(fc,args) let dest_rel0 sigma t = match EConstr.kind sigma t with @@ -351,14 +346,14 @@ let find_ring_structure env sigma l = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then CErrors.user_err ~hdr:"ring" - (str"arguments of ring_simplify do not have all the same type") + (str"Arguments of ring_simplify do not have all the same type.") in List.iter check cl'; (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> CErrors.user_err ~hdr:"ring" - (str"cannot find a declared ring structure over"++ - spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"")) + (str"Cannot find a declared ring structure over"++ + spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\".")) | [] -> assert false let add_entry e = @@ -411,16 +406,14 @@ let theory_to_obj : ring_info -> obj = ~cache:cache_th ~subst:(Some subst_th) -let setoid_of_relation env evd a r = +let setoid_of_relation env sigma a r = try - let evm = !evd in - let evm, refl = Rewrite.get_reflexive_proof env evm a r in - let evm, sym = Rewrite.get_symmetric_proof env evm a r in - let evm, trans = Rewrite.get_transitive_proof env evm a r in - evd := evm; - lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] + let sigma, refl = Rewrite.get_reflexive_proof env sigma a r in + let sigma, sym = Rewrite.get_symmetric_proof env sigma a r in + let sigma, trans = Rewrite.get_transitive_proof env sigma a r in + sigma, lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] with Not_found -> - error "cannot find setoid relation" + CErrors.user_err (str "Cannot find a setoid structure for relation " ++ pr_econstr_env env sigma r ++ str ".") let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] @@ -428,61 +421,59 @@ let op_morph r add mul opp req m1 m2 m3 = let op_smorph r add mul req m1 m2 = lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -let ring_equality env evd (r,add,mul,opp,req) = - match EConstr.kind !evd req with - | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let setoid = plapp evd coq_eq_setoid [|r|] in - let op_morph = +let ring_equality env sigma (r,add,mul,opp,req) = + match EConstr.kind sigma req with + | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) -> + let sigma, setoid = plapp sigma coq_eq_setoid [|r|] in + let sigma, op_morph = match opp with - Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] - | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let sigma = !evd in + Some opp -> plapp sigma coq_eq_morph [|r;add;mul;opp|] + | None -> plapp sigma coq_eq_smorph [|r;add;mul|] in let sigma, setoid = Typing.solve_evars env sigma setoid in let sigma, op_morph = Typing.solve_evars env sigma op_morph in - evd := sigma; (setoid,op_morph) | _ -> - let setoid = setoid_of_relation (Global.env ()) evd r req in + let sigma, setoid = setoid_of_relation env sigma r req in let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in let add_m, add_m_lem = try Rewrite.default_morphism signature add with Not_found -> - error "ring addition should be declared as a morphism" in + CErrors.user_err (str "Ring addition " ++ pr_econstr_env env sigma add ++ str " should be declared as a morphism.") in let mul_m, mul_m_lem = try Rewrite.default_morphism signature mul with Not_found -> - error "ring multiplication should be declared as a morphism" in + CErrors.user_err (str "Ring multiplication " ++ pr_econstr_env env sigma mul ++ str " should be declared as a morphism.") in let op_morph = match opp with | Some opp -> (let opp_m,opp_m_lem = try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp with Not_found -> - error "ring opposite should be declared as a morphism" in + CErrors.user_err (str "Ring opposite " ++ pr_econstr_env env sigma opp ++ str " should be declared as a morphism.") in let op_morph = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++ - str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ - str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++ - str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++ + (str"Using setoid \""++ pr_econstr_env env sigma req++str"\""++spc()++ + str"and morphisms \""++pr_econstr_env env sigma add_m ++ + str"\","++spc()++ str"\""++pr_econstr_env env sigma mul_m++ + str"\""++spc()++str"and \""++pr_econstr_env env sigma opp_m++ str"\""); op_morph) | None -> (Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ + (str"Using setoid \""++pr_econstr_env env sigma req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_econstr_env env sigma add_m ++ str"\""++spc()++str"and \""++ - pr_econstr_env env !evd mul_m_lem++str"\""); + pr_econstr_env env sigma mul_m++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) -let build_setoid_params env evd r add mul opp req eqth = +let build_setoid_params env sigma r add mul opp req eqth = match eqth with Some th -> th - | None -> ring_equality env evd (r,add,mul,opp,req) + | None -> ring_equality env sigma (r,add,mul,opp,req) let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in @@ -515,71 +506,69 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in TacArg(CAst.make (TacCall(CAst.make (t,[])))) -let make_hyp env evd c = - let t = Retyping.get_type_of env !evd c in - plapp evd coq_mkhypo [|t;c|] +let make_hyp env sigma c = + let t = Retyping.get_type_of env sigma c in + plapp sigma coq_mkhypo [|t;c|] -let make_hyp_list env evdref lH = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; - let l = +let make_hyp_list env sigma lH = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in + let sigma, l = List.fold_right - (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH - (plapp evdref coq_nil [|carrier|]) + (fun c (sigma,l) -> + let sigma, c = make_hyp env sigma c in + plapp sigma coq_cons [|carrier; c; l|]) lH + (plapp sigma coq_nil [|carrier|]) in - let sigma, l' = Typing.solve_evars env !evdref l in - evdref := sigma; + let sigma, l' = Typing.solve_evars env sigma l in let l' = EConstr.Unsafe.to_constr l' in - Evarutil.nf_evars_universes !evdref l' + sigma, Evarutil.nf_evars_universes sigma l' -let interp_power env evdref pow = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; +let interp_power env sigma pow = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in match pow with | None -> let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in - (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|]) + let sigma, c = plapp sigma coq_None [|carrier|] in + sigma, (TacArg(CAst.make (TacCall(CAst.make (t,[])))), c) | Some (tac, spec) -> let tac = match tac with | CstTac t -> Tacintern.glob_tactic t | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env evdref (ic_unsafe spec) in - (tac, plapp evdref coq_Some [|carrier; spec|]) + let spec = ic_unsafe env sigma spec in + let sigma, spec = make_hyp env sigma spec in + let sigma, pow = plapp sigma coq_Some [|carrier; spec|] in + sigma, (tac, pow) -let interp_sign env evdref sign = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; +let interp_sign env sigma sign = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in match sign with - | None -> plapp evdref coq_None [|carrier|] + | None -> plapp sigma coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evdref (ic_unsafe spec) in - plapp evdref coq_Some [|carrier;spec|] + let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in + plapp sigma coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let interp_div env evdref div = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; +let interp_div env sigma div = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in match div with - | None -> plapp evdref coq_None [|carrier|] + | None -> plapp sigma coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evdref (ic_unsafe spec) in - plapp evdref coq_Some [|carrier;spec|] + let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in + plapp sigma coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div = +let add_theory0 env sigma name rth eqth morphth cst_tac (pre,post) power sign div = check_required_library (cdir@["Ring_base"]); - let env = Global.env() in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in - let evd = ref sigma in - let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in - let (pow_tac, pspec) = interp_power env evd power in - let sspec = interp_sign env evd sign in - let dspec = interp_div env evd div in + let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in + let sigma, (pow_tac, pspec) = interp_power env sigma power in + let sigma, sspec = interp_sign env sigma sign in + let sigma, dspec = interp_div env sigma div in let rk = reflect_coeff morphth in let params,ctx = - exec_tactic env !evd 5 (zltac "ring_lemmas") + exec_tactic env sigma 5 (zltac "ring_lemmas") [sth;ext;rth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in @@ -619,16 +608,16 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div ring_post_tac = posttac }) in () -let ic_coeff_spec = function - | Computational t -> Computational (ic_unsafe t) - | Morphism t -> Morphism (ic_unsafe t) +let ic_coeff_spec env sigma = function + | Computational t -> Computational (ic_unsafe env sigma t) + | Morphism t -> Morphism (ic_unsafe env sigma t) | Abstract -> Abstract let set_once s r v = if Option.is_empty !r then r := Some v else error (s^" cannot be set twice") -let process_ring_mods l = +let process_ring_mods env sigma l = let kind = ref None in let set = ref None in let cst_tac = ref None in @@ -638,11 +627,11 @@ let process_ring_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k) + Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec env sigma k) | Const_tac t -> set_once "tactic recognizing constants" cst_tac t | Pre_tac t -> set_once "preprocess tactic" pre t | Post_tac t -> set_once "postprocess tactic" post t - | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) + | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext) | Pow_spec(t,spec) -> set_once "power" power (t,spec) | Sign_spec t -> set_once "sign" sign t | Div_spec t -> set_once "div" div t) l; @@ -650,9 +639,11 @@ let process_ring_mods l = (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) let add_theory id rth l = - let (sigma, rth) = ic rth in - let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in - add_theory0 id (sigma, rth) set k cst (pre,post) power sign div + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma, rth = ic env sigma rth in + let (k,set,cst,pre,post,power,sign, div) = process_ring_mods env sigma l in + add_theory0 env sigma id rth set k cst (pre,post) power sign div (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and @@ -663,13 +654,12 @@ let make_args_list sigma rl t = | [] -> let (_,t1,t2) = dest_rel0 sigma t in [t1;t2] | _ -> rl -let make_term_list env evd carrier rl = - let l = List.fold_right - (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl - (plapp evd coq_nil [|carrier|]) +let make_term_list env sigma carrier rl = + let sigma, l = List.fold_right + (fun x (sigma,l) -> plapp sigma coq_cons [|carrier;x;l|]) rl + (plapp sigma coq_nil [|carrier|]) in - let sigma, l = Typing.solve_evars env !evd l in - evd := sigma; l + Typing.solve_evars env sigma l let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c) let tacarg expr = @@ -695,12 +685,13 @@ let ring_lookup (f : Value.t) lH rl t = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let rl = make_args_list sigma rl t in - let evdref = ref sigma in let e = find_ring_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in + let sigma, l = make_term_list env sigma (EConstr.of_constr e.ring_carrier) rl in + let rl = Value.of_constr l in + let sigma, l = make_hyp_list env sigma lH in + let lH = carg l in let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (ring@[lH;rl])) end (***********************************************************************) @@ -758,23 +749,23 @@ let sfield_theory = my_reference "semi_field_theory" let af_ar = my_reference"AF_AR" let f_r = my_reference"F_R" let sf_sr = my_reference"SF_SR" -let dest_field env evd th_spec = - let th_typ = Retyping.get_type_of env !evd th_spec in - match EConstr.kind !evd th_typ with +let dest_field env sigma th_spec = + let th_typ = Retyping.get_type_of env sigma th_spec in + match EConstr.kind sigma th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when isRefX !evd (Lazy.force afield_theory) f -> - let rth = plapp evd af_ar + when isRefX sigma (Lazy.force afield_theory) f -> + let sigma, rth = plapp sigma af_ar [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when isRefX !evd (Lazy.force field_theory) f -> - let rth = - plapp evd f_r + when isRefX sigma (Lazy.force field_theory) f -> + let sigma, rth = + plapp sigma f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when isRefX !evd (Lazy.force sfield_theory) f -> - let rth = plapp evd sf_sr + when isRefX sigma (Lazy.force sfield_theory) f -> + let sigma, rth = plapp sigma sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) | _ -> error "bad field structure" @@ -804,14 +795,14 @@ let find_field_structure env sigma l = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then CErrors.user_err ~hdr:"field" - (str"arguments of field_simplify do not have all the same type") + (str"Arguments of field_simplify do not have all the same type.") in List.iter check cl'; (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> CErrors.user_err ~hdr:"field" - (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_econstr_env env sigma ty++str"\"")) + (str"Cannot find a declared field structure over"++ + spc()++str"\""++pr_econstr_env env sigma ty++str"\".")) | [] -> assert false let add_field_entry e = @@ -860,14 +851,14 @@ let ftheory_to_obj : field_info -> obj = ~cache:cache_th ~subst:(Some subst_th) -let field_equality evd r inv req = - match EConstr.kind !evd req with - | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> +let field_equality env sigma r inv req = + match EConstr.kind sigma req with + | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) -> let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> - let _setoid = setoid_of_relation (Global.env ()) evd r req in + let _setoid = setoid_of_relation env sigma r req in let signature = [Some (r,Some req)],Some(r,Some req) in let inv_m, inv_m_lem = try Rewrite.default_morphism signature inv @@ -875,24 +866,22 @@ let field_equality evd r inv req = error "field inverse should be declared as a morphism" in inv_m_lem -let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv = +let add_field_theory0 env sigma name fth eqth morphth cst_tac inj (pre,post) power sign odiv = let open Constr in check_required_library (cdir@["Field_tac"]); - let (sigma,fth) = ic fth in - let env = Global.env() in - let evd = ref sigma in + let (sigma,fth) = ic env sigma fth in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = - dest_field env evd fth in - let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in + dest_field env sigma fth in + let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in let eqth = Some(sth,ext) in - let _ = add_theory0 name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in - let (pow_tac, pspec) = interp_power env evd power in - let sspec = interp_sign env evd sign in - let dspec = interp_div env evd odiv in - let inv_m = field_equality evd r inv req in + let _ = add_theory0 env sigma name rth eqth morphth cst_tac (None,None) power sign odiv in + let sigma, (pow_tac, pspec) = interp_power env sigma power in + let sigma, sspec = interp_sign env sigma sign in + let sigma, dspec = interp_div env sigma odiv in + let inv_m = field_equality env sigma r inv req in let rk = reflect_coeff morphth in let params,ctx = - exec_tactic env !evd 9 (field_ltac"field_lemmas") + exec_tactic env sigma 9 (field_ltac"field_lemmas") [sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in @@ -940,7 +929,7 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od field_pre_tac = pretac; field_post_tac = posttac }) in () -let process_field_mods l = +let process_field_mods env sigma l = let kind = ref None in let set = ref None in let cst_tac = ref None in @@ -951,22 +940,24 @@ let process_field_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k) + Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec env sigma k) | Ring_mod(Const_tac t) -> set_once "tactic recognizing constants" cst_tac t | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t - | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) + | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext) | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) | Ring_mod(Sign_spec t) -> set_once "sign" sign t | Ring_mod(Div_spec t) -> set_once "div" div t - | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l; + | Inject i -> set_once "infinite property" inj (ic_unsafe env sigma i)) l; let k = match !kind with Some k -> k | None -> Abstract in - (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) + (env, sigma, k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) let add_field_theory id t mods = - let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods mods in - add_field_theory0 id t set k cst_tac inj (pre,post) power sign div + let env = Global.env () in + let sigma = Evd.from_env env in + let (env,sigma,k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods env sigma mods in + add_field_theory0 env sigma id t set k cst_tac inj (pre,post) power sign div let ltac_field_structure e = let req = carg e.field_req in @@ -987,10 +978,11 @@ let field_lookup (f : Value.t) lH rl t = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let rl = make_args_list sigma rl t in - let evdref = ref sigma in let e = find_field_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in + let sigma, c = make_term_list env sigma (EConstr.of_constr e.field_carrier) rl in + let rl = Value.of_constr c in + let sigma, l = make_hyp_list env sigma lH in + let lH = carg l in let field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (field@[lH;rl])) end diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index bd514f15d5..a4aa08300d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = - List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in + List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 00d4c7b3d8..cdf2922516 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -244,24 +244,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then - lookup_canonical_conversion (proji, Prod_cs), + lookup_canonical_conversion env (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> let s = ESorts.kind sigma s in - lookup_canonical_conversion + lookup_canonical_conversion env (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> - let c2 = GlobRef.ConstRef (Projection.constant p) in - let c = Retyping.expand_projection env sigma p c [] in - let _, args = destApp sigma c in - let sk2 = Stack.append_app args sk2 in - lookup_canonical_conversion (proji, Const_cs c2), sk2 + lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2 | _ -> let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in - lookup_canonical_conversion (proji, Const_cs c2),sk2 + lookup_canonical_conversion env (proji, Const_cs c2),sk2 with Not_found -> - let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in + let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in (c,cs),[] in let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; @@ -273,6 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = + (* Are we sure that ty is not an evar? *) try Inductiveops.find_mrectype env sigma ty with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e6e5ad8dd4..b6e44265ae 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,19 +144,21 @@ type obj_typ = { type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs -let eq_cs_pattern p1 p2 = match p1, p2 with -| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2 +let eq_cs_pattern env p1 p2 = match p1, p2 with +| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2 +| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2 | Prod_cs, Prod_cs -> true | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 | Default_cs, Default_cs -> true | _ -> false -let rec assoc_pat a = function - | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs +let rec assoc_pat env a = function + | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs | [] -> raise Not_found @@ -179,10 +181,7 @@ let rec cs_pattern_of_constr env t = patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Proj (p, c) -> - let ty = Retyping.get_type_of_constr env c in - let _, params = Inductive.find_rectype env ty in - Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] + | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (fst @@ destRef t) , None, [] @@ -238,6 +237,7 @@ let compute_canonical_projections env ~warn (gref,ind) = let pr_cs_pattern = function Const_cs c -> Nametab.pr_global_env Id.Set.empty c + | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p)) | Prod_cs -> str "_ -> _" | Default_cs -> str "_" | Sort_cs s -> Sorts.pr_sort_family s @@ -253,7 +253,7 @@ let register_canonical_structure ~warn env sigma o = compute_canonical_projections env ~warn o |> List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in - match assoc_pat cs_pat l with + match assoc_pat env cs_pat l with | exception Not_found -> object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table | _, cs -> @@ -320,8 +320,8 @@ let check_and_decompose_canonical_structure env sigma ref = error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (ref,indsp) -let lookup_canonical_conversion (proj,pat) = - assoc_pat pat (GlobRef.Map.find proj !object_table) +let lookup_canonical_conversion env (proj,pat) = + assoc_pat env pat (GlobRef.Map.find proj !object_table) let decompose_projection sigma c args = match EConstr.kind sigma c with diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3be60d5e62..5b8dc8184a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option (** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs @@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t type cs = GlobRef.t * inductive -val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ +val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit val subst_canonical_structure : Mod_subst.substitution -> cs -> cs diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 4bd22e76cb..34bcd0982c 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -67,6 +67,14 @@ let get_type_from_constraints env sigma t = | _ -> raise Not_found else raise Not_found +let sort_of_arity_with_constraints env sigma t = + try Reductionops.sort_of_arity env sigma t + with Reduction.NotArity -> + try + let t = get_type_from_constraints env sigma t in + Reductionops.sort_of_arity env sigma t + with Not_found | Reduction.NotArity -> retype_error NotAnArity + let rec subst_type env sigma typ = function | [] -> typ | h::rest -> @@ -187,9 +195,7 @@ let retype ?(polyprop=true) sigma = let mip = lookup_mind_specif env ind in let paramtyps = Array.map_to_list (fun arg () -> let t = type_of env arg in - let s = try Reductionops.sort_of_arity env sigma t - with Reduction.NotArity -> retype_error NotAnArity - in + let s = sort_of_arity_with_constraints env sigma t in Sorts.univ_of_sort (ESorts.kind sigma s)) args in diff --git a/test-suite/bugs/closed/bug_13249.v b/test-suite/bugs/closed/bug_13249.v new file mode 100644 index 0000000000..06f7ddbd3a --- /dev/null +++ b/test-suite/bugs/closed/bug_13249.v @@ -0,0 +1,9 @@ +Global Generalizable All Variables. + +Section test. + Context {A : Type}. + Context `{!foo A}. + + Goal foo A. + Proof. assumption. Defined. +End test. diff --git a/test-suite/bugs/closed/bug_13300.v b/test-suite/bugs/closed/bug_13300.v new file mode 100644 index 0000000000..e4fcd6dacc --- /dev/null +++ b/test-suite/bugs/closed/bug_13300.v @@ -0,0 +1,7 @@ +Polymorphic Definition type := Type. + +Inductive bad : type := . + +Fail Check bad : Prop. +Check bad : Set. +(* lowered as much as possible *) diff --git a/test-suite/bugs/closed/bug_13366.v b/test-suite/bugs/closed/bug_13366.v new file mode 100644 index 0000000000..06918a9266 --- /dev/null +++ b/test-suite/bugs/closed/bug_13366.v @@ -0,0 +1,5 @@ +Class Functor (F : Type -> Type) : Type := + fmap : F nat. + +Fail Definition blah := sum fmap. +(* used to be anomaly not an arity *) diff --git a/test-suite/bugs/closed/bug_9809.v b/test-suite/bugs/closed/bug_9809.v new file mode 100644 index 0000000000..4a7d2c7fac --- /dev/null +++ b/test-suite/bugs/closed/bug_9809.v @@ -0,0 +1,30 @@ +Section FreeMonad. + + Variable S : Type. + Variable P : S -> Type. + + Inductive FreeF A : Type := + | retFree : A -> FreeF A + | opr : forall s, (P s -> FreeF A) -> FreeF A. + +End FreeMonad. + +Section Fibonnacci. + + Inductive gen_op := call_op : nat -> gen_op. + Definition gen_ty (op : gen_op) := + match op with + | call_op _ => nat + end. + + Fail Definition fib0 (n:nat) : FreeF gen_op gen_ty nat := + match n with + | 0 + | 1 => retFree _ _ _ 1 + | S (S k) => + opr _ _ _ (call_op (S k)) + (fun r1 => opr _ _ _ (call_op k) + (fun r0 => retFree (* _ _ _ *) (r1 + r0))) + end. + +End Fibonnacci. diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v new file mode 100644 index 0000000000..ef526dcd7d --- /dev/null +++ b/test-suite/bugs/closed/bug_9971.v @@ -0,0 +1,27 @@ +(* Test that it raises a normal error and not an anomaly *) +Set Primitive Projections. +Record prod A B := pair { fst : A ; snd : B }. +Arguments fst {A B} _. +Arguments snd {A B} _. +Arguments pair {A B} _ _. +Record piis := { dep_types : Type; indep_args : dep_types -> Type }. +Import EqNotations. +Goal forall (id : Set) (V : id) (piiio : id -> piis) + (Z : {ridc : id & prod (dep_types (piiio ridc)) True}) + (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}), + let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in + prod True (ida V (projT1 W)) -> + Z = existT _ V (pair (projT1 W) I) -> + ida (projT1 Z) (fst (projT2 Z)). + intros. + refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + _); + refine (snd X). + Undo. +Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + snd X). +Abort. diff --git a/theories/setoid_ring/Ring_tac.v b/theories/setoid_ring/Ring_tac.v index 76e9b1e947..9323ae23b9 100644 --- a/theories/setoid_ring/Ring_tac.v +++ b/theories/setoid_ring/Ring_tac.v @@ -41,7 +41,7 @@ Ltac Get_goal := match goal with [|- ?G] => G end. Ltac OnEquation req := match goal with | |- req ?lhs ?rhs => (fun f => f lhs rhs) - | _ => (fun _ => fail "Goal is not an equation (of expected equality)") + | _ => (fun _ => fail "Goal is not an equation (of expected equality)" req) end. Ltac OnEquationHyp req h := diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index b205965ed1..d1cefeb552 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -22,9 +22,10 @@ Require Import ssreflect ssrfun. is_true b == the coercion of b : bool to Prop (:= b = true). This is just input and displayed as `b''. reflect P b == the reflection inductive predicate, asserting - that the logical proposition P : prop with the - formula b : bool. Lemmas asserting reflect P b - are often referred to as "views". + that the logical proposition P : Prop holds iff + the formula b : bool is equal to true. Lemmas + asserting reflect P b are often referred to as + "views". iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection views: iffP is used to prove reflection from logical equivalence, appP to compose views, and @@ -33,7 +34,7 @@ Require Import ssreflect ssrfun. elimT :: coercion reflect >-> Funclass, which allows the direct application of `reflect' views to boolean assertions. - decidable P <-> P is effectively decidable (:= {P} + {~ P}. + decidable P <-> P is effectively decidable (:= {P} + {~ P}). contra, contraL, ... :: contraposition lemmas. altP my_viewP :: natural alternative for reflection; given lemma myviewP: reflect my_Prop my_formula, diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 597e55a39e..8cb077ca21 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -271,9 +271,8 @@ let inductive_levels env evd arities inds = if Sorts.is_prop a || Sorts.is_sprop a then None else Some (univ_of_sort a)) destarities in - let cstrs_levels, min_levels, sizes = - CList.split3 - (List.map2 (fun (_,tys) (arity,(ctx,du)) -> + let cstrs_levels, sizes = + CList.split (List.map2 (fun (_,tys) (arity,(ctx,du)) -> let len = List.length tys in let minlev = Sorts.univ_of_sort du in let minlev = @@ -283,13 +282,15 @@ let inductive_levels env evd arities inds = in let minlev = (* Indices contribute. *) - if indices_matter env && List.length ctx > 0 then ( + if indices_matter env then begin let ilev = sign_level env evd ctx in - Univ.sup ilev minlev) + Univ.sup ilev minlev + end else minlev in let clev = extract_level env evd minlev tys in - (clev, minlev, len)) inds destarities) + (clev, len)) + inds destarities) in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) @@ -326,8 +327,13 @@ let inductive_levels env evd arities inds = let duu = Sorts.univ_of_sort du in let template_prop, evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then - if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - true, Evd.set_eq_sort env evd Sorts.prop du + if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) + then if Term.isArity arity + (* If not a syntactic arity, the universe may be used in a + polymorphic instance and so cannot be lowered to Prop. + See #13300. *) + then true, Evd.set_eq_sort env evd Sorts.prop du + else false, Evd.set_eq_sort env evd Sorts.set du else false, evd else false, Evd.set_eq_sort env evd (sort_of_univ cu) du in |