diff options
69 files changed, 257 insertions, 106 deletions
diff --git a/.travis.yml b/.travis.yml index 06ce3cae2..aa2e0e63c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,6 +37,7 @@ env: - TEST_TARGET="ci-fiat-crypto" - TEST_TARGET="ci-fiat-parsers" - TEST_TARGET="ci-flocq" + - TEST_TARGET="ci-formal-topology" - TEST_TARGET="ci-hott" - TEST_TARGET="ci-iris-coq" - TEST_TARGET="ci-math-classes" diff --git a/Makefile.ci b/Makefile.ci index 4c4606aff..013685218 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-vst ci-bedrock-src ci-bedrock-facade + ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade ci-formal-topology .PHONY: $(CI_TARGETS) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0851816c..1dfade261 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -98,13 +98,19 @@ # bedrock_src ######################################################################## : ${bedrock_src_CI_BRANCH:=master} -: ${bedrock_src_CI_GITURL:=https://github.com/JasonGross/bedrock.git} +: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git} ######################################################################## # bedrock_facade ######################################################################## : ${bedrock_facade_CI_BRANCH:=master} -: ${bedrock_facade_CI_GITURL:=https://github.com/JasonGross/bedrock.git} +: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git} + +######################################################################## +# formal-topology +######################################################################## +: ${formal_topology_CI_BRANCH:=ci} +: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} ######################################################################## # CoLoR diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh new file mode 100755 index 000000000..ecb36349f --- /dev/null +++ b/dev/ci/ci-formal-topology.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes + +Corn_CI_DIR=${CI_BUILD_DIR}/corn + +formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology + +# Setup Math-Classes + +git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} + +( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup Corn + +git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} + +( cd ${Corn_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup formal-topology + +git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} + +( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} ) diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 56ce753cd..a25da7d92 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -697,8 +697,8 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command is equivalent to the command line option {\tt -Q {\dirpath} - {\str}}. It adds the physical directory {\str} to the current {\Coq} +This command is equivalent to the command line option {\tt -Q {\str} + {\dirpath}}. It adds the physical directory {\str} to the current {\Coq} loadpath and maps it to the logical directory {\dirpath}. \begin{Variants} @@ -707,8 +707,8 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory \end{Variants} \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}} -This command is equivalent to the command line option {\tt -R {\dirpath} - {\str}}. It adds the physical directory {\str} and all its +This command is equivalent to the command line option {\tt -R {\str} + {\dirpath}}. It adds the physical directory {\str} and all its subdirectories to the current {\Coq} loadpath. \begin{Variants} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 6d54b4de1..8ba28b32f 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -118,7 +118,7 @@ the current proof and declare the initial goal as an axiom. \subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof} \label{BeginProof}} This command applies in proof editing mode. It is equivalent to {\tt - exact {\term}; Save.} That is, you have to give the full proof in + exact {\term}. Qed.} That is, you have to give the full proof in one gulp, as a proof term (see Section~\ref{exact}). \variant {\tt Proof.} diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1162b6e15..2426366c6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -430,31 +430,6 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let rec free_vars_of_pat il = - function - | CPatCstr (loc, c, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in - List.fold_left free_vars_of_pat il l2 - | CPatAtom (loc, ro) -> - begin match ro with - | Some (Ident (loc, i)) -> (loc, i) :: il - | Some _ | None -> il - end - | CPatNotation (loc, n, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (fst l1) in - List.fold_left (List.fold_left free_vars_of_pat) il (snd l1) - | _ -> anomaly (str "free_vars_of_pat") - -let intern_local_pattern intern lvar env p = - List.fold_left - (fun env (loc, i) -> - let bk = Default Implicit in - let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in - let n = Name i in - let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in - env) - env (free_vars_of_pat [] p) - let glob_local_binder_of_extended = function | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t) | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t) @@ -482,13 +457,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | Some ty -> ty | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) in - let env = intern_local_pattern intern lvar env p in - let il = List.map snd (free_vars_of_pat [] p) in - let cp = + let il,cp = match !intern_cases_pattern_fwd (None,env.scopes) p with - | (_, [(_, cp)]) -> cp + | (il, [(subst,cp)]) -> + if not (Id.Map.equal Id.equal subst Id.Map.empty) then + user_err ~loc (str "Unsupported nested \"as\" clause."); + il,cp | _ -> assert false in + let env = {env with ids = List.fold_right Id.Set.add il env.ids} in let ienv = Id.Set.elements env.ids in let id = Namegen.next_ident_away (Id.of_string "pat") ienv in let na = (loc, Name id) in @@ -945,17 +922,6 @@ let find_remaining_scopes pl1 pl2 ref = in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs), simple_adjust_scopes len_pl2 (aux (impl_list,scope_list))) -let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 - -let product_of_cases_patterns ids idspl = - List.fold_right (fun (ids,pl) (ids',ptaill) -> - (ids @ ids', - (* Cartesian prod of the or-pats for the nth arg and the tail args *) - List.flatten ( - List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) - idspl (ids,[Id.Map.empty,[]]) - (* @return the first variable that occurs twice in a pattern naive n^2 algo *) @@ -1209,6 +1175,17 @@ let alias_of als = match als.alias_ids with *) +let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 + +let product_of_cases_patterns aliases idspl = + List.fold_right (fun (ids,pl) (ids',ptaill) -> + (ids @ ids', + (* Cartesian prod of the or-pats for the nth arg and the tail args *) + List.flatten ( + List.map (fun (subst,p) -> + List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) + idspl (aliases.alias_ids,[aliases.alias_map,[]]) + let rec subst_pat_iterator y t p = match p with | RCPatAtom (_,id) -> begin match id with Some x when Id.equal x y -> t | _ -> p end @@ -1397,7 +1374,7 @@ let drop_notations_pattern looked_for = let rec intern_pat genv aliases pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in - let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in + let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in @@ -1453,7 +1430,7 @@ let intern_ind_pattern genv scopes pat = let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in (with_letin, - match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with + match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ~loc) | x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x) @@ -1777,7 +1754,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = and intern_multiple_pattern env n (loc,pl) = let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in check_number_of_pattern loc n pl; - product_of_cases_patterns [] idsl_pll + product_of_cases_patterns empty_alias idsl_pll (* Expands a disjunction of multiple pattern *) and intern_disjunctive_multiple_pattern env loc n mpl = diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 2334be966..edcfa99c8 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -361,6 +361,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst + | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> + Array.fold_left2 (sorec ctx env) subst args1 args2 | _ -> raise PatternMatchingFailure in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 33a68589c..a22db1407 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -159,7 +159,9 @@ let pattern_of_constr env sigma t = (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> PMeta None) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b08456f2f..d023b4568 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -105,6 +105,12 @@ let get_coq_eq ctx = with Not_found -> error "eq not found." +let univ_of_eq env eq = + let eq = EConstr.of_constr eq in + match kind_of_term (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with + | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false) + | _ -> assert false + (**********************************************************************) (* Check if an inductive type [ind] has the form *) (* *) @@ -761,7 +767,7 @@ let build_congr env (eq,refl,ctx) ind = let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -769,6 +775,7 @@ let build_congr env (eq,refl,ctx) ind = let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt (mkNamedLambda varB (mkSort (Type uni)) diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v index 7d0dc090e..36ab7ff59 100644 --- a/test-suite/bugs/closed/3080.v +++ b/test-suite/bugs/closed/3080.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) Delimit Scope type_scope with type. Delimit Scope function_scope with function. diff --git a/test-suite/bugs/closed/3323.v b/test-suite/bugs/closed/3323.v index 22b1603b6..4622634ea 100644 --- a/test-suite/bugs/closed/3323.v +++ b/test-suite/bugs/closed/3323.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 297 lines to 117 lines, then from 95 lines to 79 lines, then from 82 lines to 68 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3332.v b/test-suite/bugs/closed/3332.v index d86470cde..a3564bfcc 100644 --- a/test-suite/bugs/closed/3332.v +++ b/test-suite/bugs/closed/3332.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-time") -*- *) +(* -*- coq-prog-args: ("-time") -*- *) Definition foo : True. Proof. Abort. (* Toplevel input, characters 15-21: diff --git a/test-suite/bugs/closed/3346.v b/test-suite/bugs/closed/3346.v index 638404f2c..09bd78934 100644 --- a/test-suite/bugs/closed/3346.v +++ b/test-suite/bugs/closed/3346.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Monomorphic Inductive paths (A : Type) (a : A) : A -> Type := idpath : paths A a a. (* This should fail with -indices-matter *) Fail Check paths nat O O : Prop. diff --git a/test-suite/bugs/closed/3348.v b/test-suite/bugs/closed/3348.v index d9ac09d8d..904de6896 100644 --- a/test-suite/bugs/closed/3348.v +++ b/test-suite/bugs/closed/3348.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Set Printing Universes. Inductive Empty : Set := . diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index f8113e4c7..555accfd5 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -20,7 +20,7 @@ while it is expected to have type "IsHProp (* Top.17 *) Empty" Defined. Module B. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) Set Universe Polymorphism. Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. diff --git a/test-suite/bugs/closed/3375.v b/test-suite/bugs/closed/3375.v index d7ce02ea8..1e0c8e61f 100644 --- a/test-suite/bugs/closed/3375.v +++ b/test-suite/bugs/closed/3375.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *) +(* -*- mode: coq; coq-prog-args: ("-impredicative-set") -*- *) (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v index f7ab5f76a..ae8e41e29 100644 --- a/test-suite/bugs/closed/3393.v +++ b/test-suite/bugs/closed/3393.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *) Set Universe Polymorphism. Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v index 374a53928..9a57ca770 100644 --- a/test-suite/bugs/closed/3427.v +++ b/test-suite/bugs/closed/3427.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *) Generalizable All Variables. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v index d258bb31f..b0c4b2370 100644 --- a/test-suite/bugs/closed/3539.v +++ b/test-suite/bugs/closed/3539.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *) (* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0 coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *) diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 4b4f81dbc..73709268a 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *) (* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0 diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 8687eaab0..179f81e66 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index a327bbf2a..bb6af6a66 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) +(* -*- coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *) (* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *) diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v index c19a2d4a0..66dee702a 100644 --- a/test-suite/bugs/closed/3956.v +++ b/test-suite/bugs/closed/3956.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter"); mode: visual-line -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter"); mode: visual-line -*- *) Set Universe Polymorphism. Set Primitive Projections. Close Scope nat_scope. diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index e4d76732a..fc1c504f1 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -1,6 +1,6 @@ Unset Strict Universe Declaration. Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *) (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *) diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index 816bc845f..b23684671 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -1,5 +1,5 @@ Unset Strict Universe Declaration. -(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* -*- coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *) (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v index 60c935459..1ad81345d 100644 --- a/test-suite/bugs/closed/4394.v +++ b/test-suite/bugs/closed/4394.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Require Import Equality List. Inductive Foo (I : Type -> Type) (A : Type) : Type := diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v index 5c23f8404..a89cf0cbc 100644 --- a/test-suite/bugs/closed/4400.v +++ b/test-suite/bugs/closed/4400.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality. Set Printing Universes. Inductive Foo (I : Type -> Type) (A : Type) : Type := diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v index a32acf789..56a7b4f6e 100644 --- a/test-suite/bugs/closed/4456.v +++ b/test-suite/bugs/closed/4456.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) (* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *) (* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0 coqtop version 8.5beta3 (November 2015) *) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index c6fcc24b6..117d6523a 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1199 lines to 430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, then from 269 lines to 255 lines *) diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index 64c7fd8eb..c3e0da111 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) (* File reduced by coq-bug-finder from original input, then from 1125 lines to 346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, then from 285 lines to 271 lines *) diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 64dd8c304..4ad53bc62 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v index c89a86d63..a59eed2c8 100644 --- a/test-suite/bugs/closed/4656.v +++ b/test-suite/bugs/closed/4656.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal True. constructor 1. Qed. diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v index 1ae508185..10e48db6d 100644 --- a/test-suite/bugs/closed/4673.v +++ b/test-suite/bugs/closed/4673.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) (* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3 coqtop version 8.5 (February 2016) *) Axiom proof_admitted : False. diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v index f047624c8..2d41828f1 100644 --- a/test-suite/bugs/closed/4722.v +++ b/test-suite/bugs/closed/4722.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *) +(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *) diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v index 3854bbffd..cfb4548d2 100644 --- a/test-suite/bugs/closed/4727.v +++ b/test-suite/bugs/closed/4727.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0), (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) -> o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v index a6ebda61c..a90abd71c 100644 --- a/test-suite/bugs/closed/4733.v +++ b/test-suite/bugs/closed/4733.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) Require Import Coq.Lists.List. Require Import Coq.Vectors.Vector. diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v index d87906f31..33a1d1a50 100644 --- a/test-suite/bugs/closed/4769.v +++ b/test-suite/bugs/closed/4769.v @@ -1,5 +1,5 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) (* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3 coqtop version trunk (June 2016) *) diff --git a/test-suite/bugs/closed/4780.v b/test-suite/bugs/closed/4780.v index 4cec43184..71a51c631 100644 --- a/test-suite/bugs/closed/4780.v +++ b/test-suite/bugs/closed/4780.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Top" "-top" "bug_bad_induction_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1889 lines to 144 lines, then from 158 lines to 144 lines *) (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 coqtop version 8.5pl1 (April 2016) *) diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v index 9d65840ac..bbb34f465 100644 --- a/test-suite/bugs/closed/4785_compat_85.v +++ b/test-suite/bugs/closed/4785_compat_85.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *) +(* -*- coq-prog-args: ("-compat" "8.5") -*- *) Require Coq.Lists.List Coq.Vectors.Vector. Require Coq.Compat.Coq85. diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v index a91496262..fe6e65a0f 100644 --- a/test-suite/bugs/closed/4811.v +++ b/test-suite/bugs/closed/4811.v @@ -2,7 +2,7 @@ (* Submitted by Jason Gross *) -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) (* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 coqtop version 8.5pl1 (April 2016) *) diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v index 904abb228..e411ce62f 100644 --- a/test-suite/bugs/closed/4818.v +++ b/test-suite/bugs/closed/4818.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *) +(* -*- mode: coq; coq-prog-args: ("-R" "." "Prob" "-top" "Product") -*- *) (* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *) (* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3 coqtop version 8.5pl1 (June 2016) *) diff --git a/test-suite/bugs/closed/5193.v b/test-suite/bugs/closed/5193.v new file mode 100644 index 000000000..cc8739afe --- /dev/null +++ b/test-suite/bugs/closed/5193.v @@ -0,0 +1,14 @@ +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Typeclasses eauto := debug. +Set Typeclasses Debug Verbosity 2. + +Inductive Finx(n : nat) : Set := +| Fx1(i : nat)(e : n = S i) +| FxS(i : nat)(f : Finx i)(e : n = S i). + +Context `{Finx_eqdec : forall n, Eqdec (Finx n)}. + +Goal {x : Type & Eqdec x}. + eexists. + try typeclasses eauto 1 with typeclass_instances. diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v index 7254afb42..72722f5f6 100644 --- a/test-suite/bugs/closed/5198.v +++ b/test-suite/bugs/closed/5198.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 286 lines to 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from diff --git a/test-suite/bugs/closed/5300.v b/test-suite/bugs/closed/5300.v new file mode 100644 index 000000000..18202df50 --- /dev/null +++ b/test-suite/bugs/closed/5300.v @@ -0,0 +1,39 @@ +Module Test1. + + Module Type Foo. + Parameter t : unit. + End Foo. + + Module Bar : Foo. + Module Type Rnd. Definition t' : unit := tt. End Rnd. + Module Rnd_inst : Rnd. Definition t' : unit := tt. End Rnd_inst. + Definition t : unit. + exact Rnd_inst.t'. + Qed. + End Bar. + + Print Assumptions Bar.t. +End Test1. + +Module Test2. + Module Type Foo. + Parameter t1 : unit. + Parameter t2 : unit. + End Foo. + + Module Bar : Foo. + Inductive ind := . + Definition t' : unit := tt. + Definition t1 : unit. + Proof. + exact ((fun (_ : ind -> False) => tt) (fun H => match H with end)). + Qed. + Definition t2 : unit. + Proof. + exact t'. + Qed. + End Bar. + + Print Assumptions Bar.t1. + Print Assumptions Bar.t1. +End Test2. diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v new file mode 100644 index 000000000..9b995f450 --- /dev/null +++ b/test-suite/bugs/closed/5487.v @@ -0,0 +1,9 @@ +(* Was a collision between an ltac pattern variable and an evar *) + +Goal forall n, exists m, n = m :> nat. +Proof. + eexists. + Fail match goal with + | [ |- ?x = ?y ] + => match x with y => idtac end + end. diff --git a/test-suite/bugs/closed/5522.v b/test-suite/bugs/closed/5522.v new file mode 100644 index 000000000..0fae9ede4 --- /dev/null +++ b/test-suite/bugs/closed/5522.v @@ -0,0 +1,7 @@ +(* Checking support for scope delimiters and as clauses in 'pat + applied to notations with binders *) + +Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. ) + (at level 200, x binder, y binder, f at level 200). + +Check multifun '((x, y)%core as z) in (x+y,0)=z. diff --git a/test-suite/bugs/closed/HoTT_coq_012.v b/test-suite/bugs/closed/HoTT_coq_012.v index a3c697f8c..420aaf974 100644 --- a/test-suite/bugs/closed/HoTT_coq_012.v +++ b/test-suite/bugs/closed/HoTT_coq_012.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Definition UU := Type. Inductive toto (B : UU) : UU := c (x : B). diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v index 3f5d7b021..39a7103d1 100644 --- a/test-suite/bugs/closed/HoTT_coq_032.v +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *) +(* -*- mode: coq; coq-prog-args: ("-xml") -*- *) Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v index e2bf1dbed..263dec485 100644 --- a/test-suite/bugs/closed/HoTT_coq_053.v +++ b/test-suite/bugs/closed/HoTT_coq_053.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Printing Universes. Set Implicit Arguments. Generalizable All Variables. diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v index c68796593..635024e98 100644 --- a/test-suite/bugs/closed/HoTT_coq_054.v +++ b/test-suite/bugs/closed/HoTT_coq_054.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) Inductive Empty : Prop := . Inductive paths {A : Type} (a : A) : A -> Type := diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v index a25098771..561b7e557 100644 --- a/test-suite/bugs/closed/HoTT_coq_055.v +++ b/test-suite/bugs/closed/HoTT_coq_055.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Inductive Empty : Prop := . diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v index 9c7e394dc..2e6c735cf 100644 --- a/test-suite/bugs/closed/HoTT_coq_059.v +++ b/test-suite/bugs/closed/HoTT_coq_059.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x. diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index 90d1d1830..e01f73f1b 100644 --- a/test-suite/bugs/closed/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -1,6 +1,6 @@ Unset Strict Universe Declaration. Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *) Set Universe Polymorphism. Definition admit {T} : T. diff --git a/test-suite/bugs/closed/HoTT_coq_097.v b/test-suite/bugs/closed/HoTT_coq_097.v index 38e8007b6..f2b2e57b9 100644 --- a/test-suite/bugs/closed/HoTT_coq_097.v +++ b/test-suite/bugs/closed/HoTT_coq_097.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) Set Universe Polymorphism. Set Printing Universes. Inductive Empty : Set := . diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index 7c1ab8dc2..fa4072a8f 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v index b6c0da76b..ea4bcd8b4 100644 --- a/test-suite/bugs/closed/HoTT_coq_108.v +++ b/test-suite/bugs/closed/HoTT_coq_108.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *) (* File reduced by coq-bug-finder from 139 lines to 124 lines. *) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index 6ee6e6532..cd9cad406 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") *) (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *) Set Universe Polymorphism. Set Asymmetric Patterns. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v index 4530548b8..4541f13d0 100644 --- a/test-suite/bugs/opened/4803.v +++ b/test-suite/bugs/opened/4803.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) Require Import Coq.Lists.List. Require Import Coq.Vectors.Vector. diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v index 6611db70e..1e9e91979 100644 --- a/test-suite/output-modulo-time/ltacprof.v +++ b/test-suite/output-modulo-time/ltacprof.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *) +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) Ltac sleep' := do 100 (do 100 (do 100 idtac)). Ltac sleep := sleep'. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index 50131470e..3dad6271a 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v index e69e23276..b2e3c3e92 100644 --- a/test-suite/output/ErrorInModule.v +++ b/test-suite/output/ErrorInModule.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) Module M. Definition foo := nonexistent. End M. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v index 3036f8f05..505c5ce37 100644 --- a/test-suite/output/ErrorInSection.v +++ b/test-suite/output/ErrorInSection.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) Section S. Definition foo := nonexistent. End S. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 49c465b6c..52fe98ac0 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end. Check match niln in listn O return O=O with niln => eq_refl end. + +(* A test about nested "as" clauses *) +(* (was failing up to May 2017) *) + +Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v index db6348fa1..732a024fc 100644 --- a/test-suite/success/Compat84.v +++ b/test-suite/success/Compat84.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(* -*- coq-prog-args: ("-compat" "8.4") -*- *) Goal True. solve [ constructor 1 ]. Undo. diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index dd5aa81d1..855f26698 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -2,3 +2,26 @@ Scheme Induction for eq Sort Prop. Check eq_ind_dep. + +(* This was broken in v8.5 *) + +Set Rewriting Schemes. +Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a. +Unset Rewriting Schemes. + +Check myeq_rect. +Check myeq_ind. +Check myeq_rec. +Check myeq_congr. +Check myeq_sym_internal. +Check myeq_rew. +Check myeq_rew_dep. +Check myeq_rew_fwd_dep. +Check myeq_rew_r. +Check internal_myeq_sym_involutive. +Check myeq_rew_r_dep. +Check myeq_rew_fwd_r_dep. + +Set Rewriting Schemes. +Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. +Unset Rewriting Schemes. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index ce9099059..d7ec092d7 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,16 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. + +(* A variant of #2602 which was wrongly succeeding because "a", bound to + "?m", was then internally turned into a "_" in the second matching *) + +Goal exists m, S m > 0. +eexists. +Fail match goal with + | |- context [ S ?a ] => + match goal with + | |- S a > a => idtac + end +end. +Abort. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 4fca4ea18..eaf685b18 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -79,7 +79,9 @@ let pr_new_syntax po loc chan_beautify ocom = and a glimpse of the executed command *) let pp_cmd_header loc com = - let shorten s = try (String.sub s 0 30)^"..." with _ -> s in + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in let noblank s = String.map (fun c -> match c with | ' ' | '\n' | '\t' | '\r' -> '~' diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index deb2ed3e0..bf274901b 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -44,6 +44,11 @@ let rec search_cst_label lab = function | (l, SFBconst cb) :: _ when Label.equal l lab -> cb | _ :: fields -> search_cst_label lab fields +let rec search_mind_label lab = function + | [] -> raise Not_found + | (l, SFBmind mind) :: _ when Label.equal l lab -> mind + | _ :: fields -> search_mind_label lab fields + (* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: a) I don't see currently what should be used instead b) this shouldn't be critical for Print Assumption. At worse some @@ -135,6 +140,18 @@ let lookup_constant cst = else lookup_constant_in_impl cst (Some cb) with Not_found -> lookup_constant_in_impl cst None +let lookup_mind_in_impl mind = + try + let mp,dp,lab = repr_kn (canonical_mind mind) in + let fields = memoize_fields_of_mp mp in + search_mind_label lab fields + with Not_found -> + anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind) + +let lookup_mind mind = + try Global.lookup_mind mind + with Not_found -> lookup_mind_in_impl mind + (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) @@ -227,7 +244,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj = where I_0, I_1, ... are in the same mutual definition and c_ij are all their constructors. *) if Refmap_env.mem firstind_ref data then data, ax2ty else - let mib = Global.lookup_mind mind in + let mib = lookup_mind mind in (* Collects references of parameters *) let param_ctx = mib.mind_params_ctxt in let nparam = List.length param_ctx in @@ -331,7 +348,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = else accu | IndRef (m,_) | ConstructRef ((m,_),_) -> - let mind = Global.lookup_mind m in + let mind = lookup_mind m in if mind.mind_typing_flags.check_guarded then accu else |