diff options
32 files changed, 210 insertions, 62 deletions
diff --git a/.travis.yml b/.travis.yml index 7138d5c61..81f50af0a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -40,6 +40,7 @@ env: - TEST_TARGET="ci-math-comp" - TEST_TARGET="ci-sf" - TEST_TARGET="ci-unimath" + - TEST_TARGET="ci-vst" # Not ready yet for 8.7 # - TEST_TARGET="ci-cpdt" # - TEST_TARGET="ci-metacoq" @@ -49,6 +50,7 @@ matrix: allow_failures: - env: TEST_TARGET="ci-geocoq" + - env: TEST_TARGET="ci-vst" # Full Coq test-suite with two compilers # [TODO: use yaml refs and avoid duplication for packages list] diff --git a/Makefile.ci b/Makefile.ci index 897318c4d..b055ada8e 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,7 +1,7 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ - ci-unimath + ci-unimath ci-vst .PHONY: $(CI_TARGETS) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 241ec3586..336ce9d8f 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,8 +46,11 @@ ######################################################################## # HoTT ######################################################################## +# Temporal overlay : ${HoTT_CI_BRANCH:=mz-8.7} : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} +# : ${HoTT_CI_BRANCH:=master} +# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} ######################################################################## # GeoCoq @@ -74,6 +77,12 @@ : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} ######################################################################## +# VST +######################################################################## +: ${VST_CI_BRANCH:=master} +: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} + +######################################################################## # fiat_parsers ######################################################################## : ${fiat_parsers_CI_BRANCH:=master} diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 9fdd2504d..2711b7eca 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -27,11 +27,11 @@ git_checkout() # Allow an optional 4th argument for the commit local _COMMIT=${4:-FETCH_HEAD} - local _DEPTH=${5:-1} + local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi) mkdir -p ${_DEST} ( cd ${_DEST} && \ - if [ ! -d .git ] ; then git clone --depth ${_DEPTH} ${_URL} . ; fi && \ + if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \ echo "Checking out ${_DEST}" && \ git fetch ${_URL} ${_BRANCH} && \ git checkout ${_COMMIT} && \ diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index dcb46ed2a..262dd6fa0 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -17,9 +17,8 @@ read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins # Setup stdpp stdpp_CI_GITURL=${IRIS_DEP[1]}.git stdpp_CI_COMMIT=${IRIS_DEP[2]} -stdpp_CI_DEPTH="1000" -git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} ${stdpp_CI_DEPTH} +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} ( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh new file mode 100755 index 000000000..c11195185 --- /dev/null +++ b/dev/ci/ci-vst.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +VST_CI_DIR=${CI_BUILD_DIR}/VST + +# opam install -j ${NJOBS} -y menhir +git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} + +# Targets are: msl veric floyd +# Patch to avoid the upper version limit +( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} ) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index a397ca82e..bf0ce60d8 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -58,7 +58,9 @@ let rec cases_pattern_fold_names f a = function | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a - | CPatCast _ -> assert false + | CPatCast (loc,_,_) -> + CErrors.user_err_loc (loc, "cases_pattern_fold_names", + Pp.strbrk "Casts are not supported here.") let ids_of_pattern = cases_pattern_fold_names Id.Set.add Id.Set.empty diff --git a/kernel/entries.mli b/kernel/entries.mli index ea7c266bc..5287a009e 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -113,5 +113,3 @@ type side_effect = { from_env : Declarations.structure_body CEphemeron.key; eff : side_eff; } - -type side_effects = side_effect list diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index eaddace4b..b17715a8f 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1849,9 +1849,10 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel in - let n = length env.env_rel_context - n in let open Declaration in - match lookup n env.env_rel_context with + let decl = lookup n env.env_rel_context in + let n = length env.env_rel_context - n in + match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bc1cb63d8..e3b87bbe1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -206,19 +206,19 @@ let get_opaque_body env cbo = Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) type private_constant = Entries.side_effect -type private_constants = private_constant list +type private_constants = Term_typing.side_effects type private_constant_role = Term_typing.side_effect_role = | Subproof | Schema of inductive * string -let empty_private_constants = [] -let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs -let concat_private xs ys = List.fold_right add_private xs ys +let empty_private_constants = Term_typing.empty_seff +let add_private = Term_typing.add_seff +let concat_private = Term_typing.concat_seff let mk_pure_proof = Term_typing.mk_pure_proof let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects -let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) +let side_effects_of_private_constants = Term_typing.uniq_seff let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in @@ -248,7 +248,7 @@ let universes_of_private eff = | Entries.SEsubproof (c, cb, e) -> if cb.const_polymorphic then acc else Univ.ContextSet.of_context cb.const_universes :: acc) - [] eff + [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 15ebc7d88..efeb98bd2 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -47,11 +47,18 @@ type private_constant_role = | Schema of inductive * string val side_effects_of_private_constants : - private_constants -> Entries.side_effects + private_constants -> Entries.side_effect list +(** Return the list of individual side-effects in the order of their + creation. *) val empty_private_constants : private_constants val add_private : private_constant -> private_constants -> private_constants +(** Add a constant to a list of private constants. The former must be more + recent than all constants appearing in the latter, i.e. one should not + create a dependency cycle. *) val concat_private : private_constants -> private_constants -> private_constants +(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in + [e1] must be more recent than those of [e2]. *) val private_con_of_con : safe_environment -> constant -> private_constant val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b7597ba7f..6ce14c853 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,8 +24,6 @@ open Fast_typeops (* Insertion of constants and parameters in environment. *) -let mk_pure_proof c = (c, Univ.ContextSet.empty), [] - let equal_eff e1 e2 = let open Entries in match e1, e2 with @@ -37,13 +35,54 @@ let equal_eff e1 e2 = cl1 cl2 | _ -> false -let rec uniq_seff = function - | [] -> [] - | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) -(* The list of side effects is in reverse order (most recent first). - * To keep the "topological" order between effects we have to uniq-ize from - * the tail *) -let uniq_seff l = List.rev (uniq_seff (List.rev l)) +module SideEffects : +sig + type t + val repr : t -> side_effect list + val empty : t + val add : side_effect -> t -> t + val concat : t -> t -> t +end = +struct + +let compare_seff e1 e2 = match e1, e2 with +| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2 +| SEscheme (cl1, _), SEscheme (cl2, _) -> + let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in + CList.compare cmp cl1 cl2 +| SEsubproof _, SEscheme _ -> -1 +| SEscheme _, SEsubproof _ -> 1 + +module SeffOrd = struct +type t = side_effect +let compare e1 e2 = compare_seff e1.eff e2.eff +end + +module SeffSet = Set.Make(SeffOrd) + +type t = { seff : side_effect list; elts : SeffSet.t } +(** Invariant: [seff] is a permutation of the elements of [elts] *) + +let repr eff = eff.seff +let empty = { seff = []; elts = SeffSet.empty } +let add x es = + if SeffSet.mem x es.elts then es + else { seff = x :: es.seff; elts = SeffSet.add x es.elts } +let concat xes yes = + List.fold_right add xes.seff yes + +end + +type side_effects = SideEffects.t + +let uniq_seff_rev = SideEffects.repr +let uniq_seff l = List.rev (SideEffects.repr l) + +let empty_seff = SideEffects.empty +let add_seff = SideEffects.add +let concat_seff = SideEffects.concat + +let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff let inline_side_effects env body ctx side_eff = let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = @@ -97,7 +136,7 @@ let inline_side_effects env body ctx side_eff = t, ctx, (mb,List.length cbl) :: sl in (* CAVEAT: we assure a proper order *) - List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff) + List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff) (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct *) @@ -381,7 +420,7 @@ let constant_entry_of_side_effect cb u = | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, []); + const_entry_body = Future.from_val (pt, empty_seff); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = @@ -415,7 +454,7 @@ let export_side_effects mb env ce = let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~greedy:true ~pure:true body - (fun (b_ctx, _) -> b_ctx, []) } in + (fun (b_ctx, _) -> b_ctx, empty_seff) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -427,7 +466,7 @@ let export_side_effects mb env ce = let cbl = List.filter not_exists cbl in if cbl = [] then acc, sl else cbl :: acc, (mb,List.length cbl) :: sl in - let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in + let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in let trusted = check_signatures mb signatures in let push_seff env = function | kn, cb, `Nothing, _ -> @@ -500,7 +539,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), []); + (body, ctx'), empty_seff); } let inline_side_effects env body side_eff = diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 89b5fc40e..075389ea5 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,6 +12,8 @@ open Environ open Declarations open Entries +type side_effects + val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes @@ -29,7 +31,15 @@ val inline_entry_side_effects : {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val uniq_seff : side_effects -> side_effects +val empty_seff : side_effects +val add_seff : side_effect -> side_effects -> side_effects +val concat_seff : side_effects -> side_effects -> side_effects +(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in + [e1] must be more recent than those of [e2]. *) +val uniq_seff : side_effects -> side_effect list +(** Return the list of individual side-effects in the order of their + creation. *) + val equal_eff : side_effect -> side_effect -> bool val translate_constant : diff --git a/lib/future.ml b/lib/future.ml index ea0382a63..ca73d5e39 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -151,8 +151,8 @@ let chain ~pure ck f = create ~uuid ~name fix_exn (match !c with | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck)) | Exn _ as x -> x - | Val (v, None) when pure -> Closure (fun () -> f v) - | Val (v, Some _) when pure -> Closure (fun () -> f v) + | Val (v, None) when pure -> Val (f v, None) + | Val (v, Some _) when pure -> Val (f v, None) | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v) | Val (v, None) -> match !ck with diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index 5cbddc7f6..698c913e8 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -108,6 +108,8 @@ let string_get s i = try Proofview.NonLogical.return (String.get s i) with e -> Proofview.NonLogical.raise e +let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com") + (* Gives the number of steps or next breakpoint of a run command *) let run_com inst = let open Proofview.NonLogical in @@ -118,14 +120,14 @@ let run_com inst = let s = String.sub inst i (String.length inst - i) in if inst.[0] >= '0' && inst.[0] <= '9' then int_of_string s >>= fun num -> - (if num<0 then invalid_arg "run_com" else return ()) >> + (if num<0 then run_invalid_arg () else return ()) >> (skip:=num) >> (skipped:=0) else breakpoint:=Some (possibly_unquote s) else - invalid_arg "run_com" + run_invalid_arg () else - invalid_arg "run_com" + run_invalid_arg () (* Prints the run counter *) let run ini = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ef3e53bf1..17779d25b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -554,31 +554,30 @@ let dependencies_in_rhs nargs current tms eqns = declarations [d(i+1);...;dn] the term [tmi] is dependent in. [find_dependencies_signature (used1,...,usedn) ((tm1,d1),...,(tmn,dn))] - returns [(deps1,...,depsn)] where [depsi] is a subset of n,..,i+1 + returns [(deps1,...,depsn)] where [depsi] is a subset of tm(i+1),..,tmn denoting in which of the d(i+1)...dn, the term tmi is dependent. - Dependencies are expressed by index, e.g. in dependency list - [n-2;1], [1] points to [dn] and [n-2] to [d3] *) let rec find_dependency_list tmblock = function | [] -> [] - | (used,tdeps,d)::rest -> + | (used,tdeps,tm,d)::rest -> let deps = find_dependency_list tmblock rest in if used && List.exists (fun x -> dependent_decl x d) tmblock then - List.add_set Int.equal - (List.length rest + 1) (List.union Int.equal deps tdeps) + match kind_of_term tm with + | Rel n -> List.add_set Int.equal n (List.union Int.equal deps tdeps) + | _ -> List.union Int.equal deps tdeps else deps let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist = let deps = find_dependency_list (tm::tmtypleaves) nextlist in if is_dep_or_cstr_in_rhs || not (List.is_empty deps) - then ((true ,deps,d)::nextlist) - else ((false,[] ,d)::nextlist) + then ((true ,deps,tm,d)::nextlist) + else ((false,[] ,tm,d)::nextlist) let find_dependencies_signature deps_in_rhs typs = let l = List.fold_right2 find_dependencies deps_in_rhs typs [] in - List.map (fun (_,deps,_) -> deps) l + List.map (fun (_,deps,_,_) -> deps) l (* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |- and xn:Tn has just been regeneralized into x:Tn so that the terms diff --git a/stm/stm.ml b/stm/stm.ml index 71ec8acc6..822229f47 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1746,12 +1746,13 @@ end = struct (* {{{ *) { indentation; verbose; loc; expr = e; strlen } = let e, time, fail = - let rec find time fail = function - | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e - | VernacFail e -> find time true e - | _ -> e, time, fail in find false false e in + let rec find ~time ~fail = function + | VernacTime (_,e) -> find ~time:true ~fail e + | VernacRedirect (_,(_,e)) -> find ~time ~fail e + | VernacFail e -> find ~time ~fail:true e + | e -> e, time, fail in find ~time:false ~fail:false e in Hooks.call Hooks.with_fail fail (fun () -> - (if time then System.with_time false else (fun x -> x)) (fun () -> + (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let goals, _, _, _, _ = Proof.proof p in @@ -2140,10 +2141,13 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - resilient_command reach view.next; - vernac_interp id x; - if eff then update_global_env () - ), (if eff then `Yes else cache), true + (match !Flags.async_proofs_mode with + | Flags.APon | Flags.APonLazy -> + resilient_command reach view.next + | Flags.APoff -> reach view.next); + vernac_interp id x; + if eff then update_global_env () + ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; vernac_interp id x; diff --git a/test-suite/bugs/closed/4957.v b/test-suite/bugs/closed/4957.v new file mode 100644 index 000000000..0efd87ac0 --- /dev/null +++ b/test-suite/bugs/closed/4957.v @@ -0,0 +1,6 @@ +Ltac get_value H := eval cbv delta [H] in H. + +Goal True. +refine (let X := _ in _). +let e := get_value X in unify e Prop. +Abort. diff --git a/test-suite/bugs/closed/5435.v b/test-suite/bugs/closed/5435.v new file mode 100644 index 000000000..60ace5ce9 --- /dev/null +++ b/test-suite/bugs/closed/5435.v @@ -0,0 +1,2 @@ +Definition foo (x : nat) := Eval native_compute in x. + diff --git a/test-suite/bugs/closed/5460.v b/test-suite/bugs/closed/5460.v new file mode 100644 index 000000000..50221cdd8 --- /dev/null +++ b/test-suite/bugs/closed/5460.v @@ -0,0 +1,11 @@ +(* Bugs in computing dependencies in pattern-matching compilation *) + +Inductive A := a1 | a2. +Inductive B := b. +Inductive C : A -> Type := c : C a1 | d : C a2. +Definition P (x : A) (y : C x) (z : B) : nat := + match z, x, y with + | b, a1, c => 0 + | b, a2, d => 0 + | _, _, _ => 1 + end. diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out new file mode 100644 index 000000000..851ecd930 --- /dev/null +++ b/test-suite/output/ErrorInModule.out @@ -0,0 +1,2 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v new file mode 100644 index 000000000..e69e23276 --- /dev/null +++ b/test-suite/output/ErrorInModule.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Module M. + Definition foo := nonexistent. +End M. diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out new file mode 100644 index 000000000..851ecd930 --- /dev/null +++ b/test-suite/output/ErrorInSection.out @@ -0,0 +1,2 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v new file mode 100644 index 000000000..3036f8f05 --- /dev/null +++ b/test-suite/output/ErrorInSection.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Section S. + Definition foo := nonexistent. +End S. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out new file mode 100644 index 000000000..128bc7767 --- /dev/null +++ b/test-suite/output/UnivBinders.out @@ -0,0 +1,6 @@ +bar@{u} = nat + : Wrap@{u} Set +(* u |= Set < u + *) + +bar is universe polymorphic diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v new file mode 100644 index 000000000..d9e89e43c --- /dev/null +++ b/test-suite/output/UnivBinders.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Class Wrap A := wrap : A. + +Instance bar@{u} : Wrap@{u} Set. Proof nat. +Print bar. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 52acad746..837f2efd0 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -121,6 +121,7 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). Goal True. {{ exact I. }} Qed. + Check |- {{ 0 }} 0. (* Check parsing of { and } is not affected by notations #3479 *) @@ -135,3 +136,9 @@ Notation "" := (@nil) (only printing). (* Check that a notation cannot be neither parsing nor printing. *) Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing). + +(* Check "where" clause for inductive types with parameters *) + +Reserved Notation "x === y" (at level 50). +Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x + where "x === y" := (EQ x y). diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v index 048b53d26..fe3b8c1d7 100644 --- a/test-suite/success/univnames.v +++ b/test-suite/success/univnames.v @@ -21,6 +21,17 @@ Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. +Class Wrap A := wrap : A. + +Fail Instance bad@{} : Wrap Type := Type. + +Instance bad@{} : Wrap Type. +Fail Proof Type. +Abort. + +Instance bar@{u} : Wrap@{u} Set. Proof nat. + + Monomorphic Universe g. -Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file +Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 85123cc44..b32985b80 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -243,9 +243,9 @@ Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) (at level 200, x ident, p at level 200, right associativity) : type_scope. -Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q)) - (at level 200, x ident, t at level 200, p at level 200, right associativity, - format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'") +Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q)) + (at level 200, x ident, A at level 200, p at level 200, right associativity, + format "'[' 'exists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") : type_scope. (** Derived rules for universal quantification *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 1528cbb2f..8142d48d8 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -332,7 +332,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p the refinement manually.*) let gls = List.rev (Evd.future_goals evm) in let evm = Evd.reset_future_goals evm in - Lemmas.start_proof id kind evm termtype + Lemmas.start_proof id ?pl kind evm termtype (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) diff --git a/toplevel/command.ml b/toplevel/command.ml index a9f2598e2..93f156ee2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -591,12 +591,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in + let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6736d8329..3df6d7a58 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2218,7 +2218,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v | VernacRedirect (s, (_,v)) -> - Feedback.with_output_to_file s (aux false) v + Feedback.with_output_to_file s (aux ?locality ?polymorphism isprogcmd) v | VernacTime (_,v) -> System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v; |