From bbef0e8702bf5e2dcad9bb4c47f92858d4eea9b4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Nov 2015 11:02:40 +0100 Subject: Fixing documention of Add Printing Coercion. --- doc/refman/Coercion.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index e4aa69353d..16006a6adf 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -312,12 +312,13 @@ Conversely, to skip the printing of coercions, use {\tt Unset Printing Coercions}. By default, coercions are not printed. -\asubsection{\tt Set Printing Coercion {\qualid}.} -\optindex{Printing Coercion} +\asubsection{\tt Add Printing Coercion {\qualid}.} +\comindex{Add Printing Coercion} +\comindex{Remove Printing Coercion} This command forces coercion denoted by {\qualid} to be printed. To skip the printing of coercion {\qualid}, use - {\tt Unset Printing Coercion {\qualid}}. + {\tt Remove Printing Coercion {\qualid}}. By default, a coercion is never printed. \asection{Classes as Records} -- cgit v1.2.3 From e9f1b6abaf062e8fbb4892f7ec8856dcf81c2757 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 31 Oct 2015 15:12:02 +0100 Subject: Tests for syntax "Show id" and [id]:tac (shelved or not). --- test-suite/success/destruct.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 83a33f75dc..59cd25cd76 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -97,6 +97,7 @@ Abort. Goal exists x, S x = S 0. eexists. +Show x. (* Incidentally test Show on a named goal *) destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S 0). Abort. @@ -105,6 +106,7 @@ Goal exists x, S 0 = S x. eexists. destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S ?x). +[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. -- cgit v1.2.3 From eec77191b33bbca4c9d8b1b92b0c622ef430a3a8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 1 Nov 2015 11:20:34 +0100 Subject: Preservation of the name of evars/goals when applying pose/set/intro/clearbody. For pose/set/clearbody, I think it is clear that we want to preserve the name and this commit do it. For revert, I first did not preserve the name, then considered in 2ba2ca96be88 that it was better to preserve it. For intro, like for revert actually, I did not preserve the name, based on the idea that the type was changing (*). For instance if we have ?f:nat->nat, do we really want to keep the name f in ?f:nat after an intro. For revert, I changed my mind based on the idea that if we had a better control of the name if we keep the name that if the system invents a new one based on the type. I think this is more reasonable than (*), so this commit preserves the name for intro. For generalize, it is still not done because of generalize being in the old proof engine. --- tactics/tactics.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e215ff42f9..37b715ebe2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -164,7 +164,7 @@ let unsafe_intro env store (id, c, t) b = let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar id) b in - let sigma, ev = new_evar_instance nctx sigma nb ~store ninst in + let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in sigma, mkNamedLambda_or_LetIn (id, c, t) ev end @@ -1834,7 +1834,7 @@ let clear_body ids = in check_hyps <*> check_concl <*> Proofview.Refine.refine ~unsafe:true begin fun sigma -> - Evarutil.new_evar env sigma concl + Evarutil.new_evar env sigma ~principal:true concl end end @@ -2599,7 +2599,7 @@ let new_generalize_gen_let lconstr = in Proofview.Unsafe.tclEVARS sigma <*> Proofview.Refine.refine begin fun sigma -> - let (sigma, ev) = Evarutil.new_evar env sigma newcl in + let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in (sigma, (applist (ev, args))) end end -- cgit v1.2.3 From 9e0cabdaf2055a9bef075d122260a96bb51df2aa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Nov 2015 23:06:14 +0100 Subject: Fixing output test Existentials.v after eec77191b. --- test-suite/output/Existentials.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 483a9ea792..52e1e0ed01 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,5 +1,5 @@ Existential 1 = -?Goal0 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] Existential 2 = ?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) -Existential 3 = ?e : [q : nat n : nat m : nat |- n = ?y] +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] -- cgit v1.2.3 From b3aba0467a99ce8038816b845cf883be3521fce8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 Nov 2015 13:39:00 +0100 Subject: Pushing the backtrace in conversion anomalies. --- pretyping/reductionops.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 0714c93b4f..156c9a2772 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1251,13 +1251,18 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV +let report_anomaly _ = + let e = UserError ("", Pp.str "Conversion test raised an anomaly") in + let e = Errors.push e in + iraise e + let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in let _ = f ~evars reds env (Evd.universes sigma) x y in true with Reduction.NotConvertible -> false - | e when is_anomaly e -> error "Conversion test raised an anomaly" + | e when is_anomaly e -> report_anomaly e let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma @@ -1275,7 +1280,7 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false - | e when is_anomaly e -> error "Conversion test raised an anomaly" + | e when is_anomaly e -> report_anomaly e let sigma_compare_sorts env pb s0 s1 sigma = match pb with @@ -1316,7 +1321,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with | Reduction.NotConvertible -> sigma, false | Univ.UniverseInconsistency _ when catch_incon -> sigma, false - | e when is_anomaly e -> error "Conversion test raised an anomaly" + | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) -- cgit v1.2.3 From 08fa634493b8635a77174bbdcd0e1529e3c40279 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 Nov 2015 18:43:50 +0100 Subject: Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly. --- tactics/tactics.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 37b715ebe2..0a013e95f7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2345,7 +2345,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let t = match ty with Some t -> t | _ -> typ_of env sigma c in + let (sigma, t) = match ty with + | Some t -> (sigma, t) + | None -> + let t = typ_of env sigma c in + Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t + in let eq_tac gl = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with -- cgit v1.2.3 From 5587499e721f4aa1f2cf35596a8f7aa58d852592 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 Nov 2015 11:17:20 +0100 Subject: Test for bug #4404. --- test-suite/bugs/closed/4404.v | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 test-suite/bugs/closed/4404.v diff --git a/test-suite/bugs/closed/4404.v b/test-suite/bugs/closed/4404.v new file mode 100644 index 0000000000..27b43a61d4 --- /dev/null +++ b/test-suite/bugs/closed/4404.v @@ -0,0 +1,4 @@ +Inductive Foo : Type -> Type := foo A : Foo A. +Goal True. + remember Foo. + -- cgit v1.2.3 From bde12b7066d7d1f3849d529428b2be3343a27787 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 6 Nov 2015 17:37:42 +0100 Subject: Fixing a bug in reporting ill-formed constructor. For instance, Inductive a (x:=1) := C : a -> True. was wrongly reporting Error: The type of constructor C is not valid; its conclusion must be "a" applied to its parameter. Also "simplifying" explain_ind_err. --- kernel/indtypes.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8b03df64c6..5e899d07be 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -337,7 +337,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor + | LocalNotConstructor of rel_context * constr list | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -348,7 +348,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env nbpar c nargs err = +let explain_ind_err id ntyp env nbpar c err = let (lpar,c') = mind_extract_params nbpar c in match err with | LocalNonPos kt -> @@ -356,9 +356,11 @@ let explain_ind_err id ntyp env nbpar c nargs err = | LocalNotEnoughArgs kt -> raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) - | LocalNotConstructor -> + | LocalNotConstructor (paramsctxt,args)-> + let nparams = rel_context_nhyps paramsctxt in raise (InductiveError - (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs))) + (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, + List.length args - nparams))) | LocalNonPar (n,i,l) -> raise (InductiveError (NonPar (env,c',n,mkRel i, mkRel (l+nbpar)))) @@ -547,7 +549,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname begin match hd with | Rel j when Int.equal j (n + ntypes - i - 1) -> check_correct_par ienv hyps (ntypes - i) largs - | _ -> raise (IllFormedInd LocalNotConstructor) + | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,largs))) end else if not (List.for_all (noccur_between n ntypes) largs) @@ -563,7 +565,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname try check_constructors ienv true nmr rawc with IllFormedInd err -> - explain_ind_err id (ntypes-i) env lparams c nargs err) + explain_ind_err id (ntypes-i) env lparams c err) (Array.of_list lcnames) indlc in let irecargs = Array.map snd irecargs_nmr -- cgit v1.2.3 From 1b163c6230ecd78526bb404fb2b7cc04985df2d9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Oct 2015 17:29:28 +0200 Subject: Typo. --- tactics/ftactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index fea0432aea..a688b94879 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -16,7 +16,7 @@ type 'a focus = (** Type of tactics potentially goal-dependent. If it contains a [Depends], then the length of the inner list is guaranteed to be the number of - currently focussed goals. Otherwise it means the tactic does not depends + currently focussed goals. Otherwise it means the tactic does not depend on the current set of focussed goals. *) type 'a t = 'a focus Proofview.tactic -- cgit v1.2.3 From ab1d8792143a05370a1efe3d19469c25b82d7097 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 6 Nov 2015 16:33:29 +0100 Subject: Dead code from the commit having introduced primitive projections (a4043608). --- kernel/indtypes.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5e899d07be..351de9ee88 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -112,18 +112,18 @@ let is_unit constrsinfos = | [] -> (* type without constructors *) true | _ -> false -let infos_and_sort env ctx t = - let rec aux env ctx t max = +let infos_and_sort env t = + let rec aux env t max = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in let env1 = Environ.push_rel (name,None,varj.utj_val) env in let max = Universe.sup max (univ_of_sort varj.utj_type) in - aux env1 ctx c2 max + aux env1 c2 max | _ when is_constructor_head t -> max | _ -> (* don't fail if not positive, it is tested later *) max - in aux env ctx t Universe.type0m + in aux env t Universe.type0m (* Computing the levels of polymorphic inductive types @@ -148,14 +148,14 @@ let infos_and_sort env ctx t = (* This (re)computes informations relevant to extraction and the sort of an arity or type constructor; we do not to recompute universes constraints *) -let infer_constructor_packet env_ar_par ctx params lc = +let infer_constructor_packet env_ar_par params lc = (* type-check the constructors *) let jlc = List.map (infer_type env_ar_par) lc in let jlc = Array.of_list jlc in (* generalize the constructor over the parameters *) let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) - let levels = List.map (infos_and_sort env_ar_par ctx) lc in + let levels = List.map (infos_and_sort env_ar_par) lc in let isunit = is_unit levels in let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in let level = List.fold_left (fun max l -> Universe.sup max l) min levels in @@ -261,8 +261,7 @@ let typecheck_inductive env mie = List.fold_right2 (fun ind arity_data inds -> let (lc',cstrs_univ) = - infer_constructor_packet env_ar_par ContextSet.empty - params ind.mind_entry_lc in + infer_constructor_packet env_ar_par params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in let ind' = (arity_data,consnames,lc',cstrs_univ) in ind'::inds) -- cgit v1.2.3