From 6ebd2316e5acf10e0d505804fdd7001edc5575fa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 May 2015 11:54:49 +0200 Subject: Making the strategy type in Rewrite opaque. --- tactics/rewrite.mli | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index cae00f5a86..40a18ac458 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -55,10 +55,7 @@ type rewrite_result = | Identity | Success of rewrite_result_info -type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types -> - (bool (* prop *) * constr option) -> evars -> 'a * rewrite_result - -type strategy = unit pure_strategy +type strategy val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy -- cgit v1.2.3 From e4ca462b7d51f25b258263345835025c1c4325bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 May 2015 12:28:42 +0200 Subject: Removing dead code in Rewrite. The hypinfo cache was actually always set to None, so that there was no need to try to preserve it if it was set to an actual value. --- tactics/rewrite.ml | 64 ++++++++++++++++++++---------------------------------- 1 file changed, 23 insertions(+), 41 deletions(-) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 60ce0e0dc3..1be394aa4a 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -452,7 +452,6 @@ let convertible env evd x y = Reductionops.is_conv_leq env evd x y type hypinfo = { - env : env; prf : constr; car : constr; rel : constr; @@ -498,7 +497,7 @@ let decompose_applied_relation env sigma (c,l) = let sort = sort_of_rel env sigma equiv in let args = Array.map_of_list (fun h -> h.Clenv.hole_evar) holes in let value = mkApp (c, args) in - Some (sigma, { env=env; prf=value; + Some (sigma, { prf=value; car=ty1; rel = equiv; sort = Sorts.is_prop sort; c1=c1; c2=c2; holes }) in @@ -510,10 +509,6 @@ let decompose_applied_relation env sigma (c,l) = | Some c -> c | None -> error "Cannot find an homogeneous relation to rewrite." -let decompose_applied_relation_expr env sigma (is, (c,l)) = - let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in - decompose_applied_relation env sigma cbl - let rewrite_db = "rewrite" let conv_transparent_state = (Id.Pred.empty, Cpred.full) @@ -588,24 +583,12 @@ let general_rewrite_unif_flags () = Unification.resolve_evars = true } -let refresh_hypinfo env sigma hypinfo c = - let sigma, hypinfo = match hypinfo with - | None -> - decompose_applied_relation_expr env sigma c - | Some hypinfo -> - if hypinfo.env != env then - (* If the lemma actually generates existential variables, we cannot - use it here as it will polute the evar map with existential variables - that might not ever get instantiated (e.g. if we rewrite under a - binder and need to refresh [c] again) *) - (* TODO: remove bindings in sigma corresponding to c *) - decompose_applied_relation_expr env sigma c - else sigma, hypinfo - in +let refresh_hypinfo env sigma (is, cb) = + let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma cb in + let sigma, hypinfo = decompose_applied_relation env sigma cbl in let { c1; c2; car; rel; prf; sort; holes } = hypinfo in sigma, (car, rel, prf, c1, c2, holes, sort) - (** FIXME: write this in the new monad interface *) let solve_remaining_by env sigma holes by = match by with @@ -719,7 +702,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = let rew_prf = RewPrf (rel, prf) in let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in let rew = if l2r then rew else symmetry env sort rew in - Some ((), rew) + Some rew with | e when Class_tactics.catchable e -> None | Reduction.NotConvertible -> None @@ -829,27 +812,27 @@ let coerce env avoid cstr res = let rel, prf = get_rew_prf res in apply_constraint env avoid res.rew_car rel prf cstr res -let apply_rule unify loccs : ('a * int) pure_strategy = +let apply_rule unify loccs : int pure_strategy = let (nowhere_except_in,occs) = convert_occs loccs in let is_occ occ = if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in - fun (hypinfo, occ) env avoid t ty cstr evars -> - let unif = if isEvar t then None else unify hypinfo env evars t in + fun occ env avoid t ty cstr evars -> + let unif = if isEvar t then None else unify env evars t in match unif with - | None -> ((hypinfo, occ), Fail) - | Some (hypinfo', rew) -> + | None -> (occ, Fail) + | Some rew -> let occ = succ occ in - if not (is_occ occ) then ((hypinfo, occ), Fail) - else if eq_constr t rew.rew_to then ((hypinfo, occ), Identity) + if not (is_occ occ) then (occ, Fail) + else if eq_constr t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in let rel, prf = get_rew_prf res in let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in - ((hypinfo', occ), res) - + (occ, res) + let apply_lemma l2r flags oc by loccs : strategy = fun () env avoid t ty cstr (sigma, cstrs) -> let sigma, c = oc sigma in @@ -857,13 +840,13 @@ let apply_lemma l2r flags oc by loccs : strategy = let { c1; c2; car; rel; prf; sort; holes } = hypinfo in let rew = (car, rel, prf, c1, c2, holes, sort) in let evars = (sigma, cstrs) in - let unify () env evars t = + let unify env evars t = let rew = unify_eqn rew l2r flags env evars by t in match rew with | None -> None - | Some rew -> Some ((), rew) + | Some rew -> Some rew in - let _, res = apply_rule unify loccs ((), 0) env avoid t ty cstr evars in + let _, res = apply_rule unify loccs 0 env avoid t ty cstr evars in (), res let e_app_poly env evars f args = @@ -1379,11 +1362,10 @@ end let rewrite_with l2r flags c occs : strategy = fun () env avoid t ty cstr (sigma, cstrs) -> - let hypinfo = None in - let unify hypinfo env evars t = + let unify env evars t = let (sigma, cstrs) = evars in let ans = - try Some (refresh_hypinfo env sigma hypinfo c) + try Some (refresh_hypinfo env sigma c) with e when Class_tactics.catchable e -> None in match ans with @@ -1392,14 +1374,14 @@ let rewrite_with l2r flags c occs : strategy = let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in match rew with | None -> None - | Some rew -> Some (None, rew) (** reset the hypinfo cache *) + | Some rew -> Some rew in let app = apply_rule unify occs in let strat = Strategies.fix (fun aux -> Strategies.choice app (subterm true default_flags aux)) in - let _, res = strat (hypinfo, 0) env avoid t ty cstr (sigma, cstrs) in + let _, res = strat 0 env avoid t ty cstr (sigma, cstrs) in ((), res) let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars = @@ -1967,12 +1949,12 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in - let unify () env evars t = unify_abs res l2r sort env evars t in + let unify env evars t = unify_abs res l2r sort env evars t in let app = apply_rule unify occs in let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in let substrat = Strategies.fix recstrat in let strat () env avoid t ty cstr evars = - let _, res = substrat ((), 0) env avoid t ty cstr evars in + let _, res = substrat 0 env avoid t ty cstr evars in (), res in let origsigma = project gl in -- cgit v1.2.3 From 8d3fd3aa8029fa7c5acb3118846cf18ffe752b9c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 5 May 2015 13:21:04 +0200 Subject: Fix bug #4212, congruence forgetting about some universe constraints. --- plugins/cc/cctac.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 05f4c49030..9952cb0807 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -253,6 +253,12 @@ let new_app_global f args k = let new_refine c = Proofview.V82.tactic (refine c) +let assert_before n c = + Proofview.Goal.enter begin fun gl -> + let evm, _ = Tacmach.New.pf_apply e_type_of gl c in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) + end + let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> let type_of t = Tacmach.New.pf_type_of gl t in -- cgit v1.2.3 From ff58f3d68369e0e535a98326e53de782ff460096 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 May 2015 17:47:11 +0200 Subject: Granting wish #4221. --- ide/wg_ProofView.ml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b12d29d6c9..a5faa60a81 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -162,12 +162,21 @@ let display mode (view : #GText.view_skel) goals hints evars = List.iter iter shelved_goals | _, _, _, _ -> (* No foreground proofs, but still unfocused ones *) - view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n"; - let iter goal = + let total = List.length bg in + let goal_str index = Printf.sprintf + "______________________________________(%d/%d)\n" index total + in + let vb, pl = if total = 1 then "is", "" else "are", "s" in + let msg = Printf.sprintf "This subproof is complete, but there %s still %d \ + unfocused goal%s:\n\n" vb total pl + in + let () = view#buffer#insert msg in + let iter i goal = + let () = view#buffer#insert (goal_str (succ i)) in let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in view#buffer#insert msg in - List.iter iter bg + List.iteri iter bg end | Some { Interface.fg_goals = fg } -> mode view fg hints -- cgit v1.2.3 From a72b7db875780ccc84b9359ffa66c170cfe6ebfd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 5 May 2015 19:19:08 +0200 Subject: Compatibility ocaml 3.12. --- ide/wg_ProofView.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index a5faa60a81..1f3fa3ed36 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util + class type proof_view = object inherit GObj.widget -- cgit v1.2.3 From 5a0d3395cd972393eaa7859f47a738cc99ea55c6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 6 May 2015 12:35:42 +0200 Subject: Fixing "subst" to respect v8.4 most-ancient to most-recent hyps order after patch for #4214 on subst needed to be repeated (see 857e82b2ca0d1). --- tactics/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index f2860a2300..c5b87761d8 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1681,7 +1681,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = with Constr_matching.PatternMatchingFailure -> None in let hyps = Proofview.Goal.hyps gl in - List.map_filter test hyps + List.rev (List.map_filter test hyps) in (* Second step: treat equations *) -- cgit v1.2.3 From 32a9a4e3656e581af41c26f48f63ed1daec331d8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 6 May 2015 18:54:18 +0200 Subject: Fixing treatment of recursive equations damaged by 857e82b2ca0d1. Improving treatment of recursive equations compared to 8.4 (see test-suite). Experimenting not to unfold local defs ever in subst. (+ Slight simplification in checking reflexive equalities only once). --- tactics/equality.ml | 18 +++++++++++------- test-suite/success/subst.v | 25 +++++++++++++++++++++++++ 2 files changed, 36 insertions(+), 7 deletions(-) create mode 100644 test-suite/success/subst.v diff --git a/tactics/equality.ml b/tactics/equality.ml index c5b87761d8..591fbabaef 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1667,17 +1667,18 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* First step: find hypotheses to treat in linear time *) let find_equations gl = let gl = Proofview.Goal.assume gl in + let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in let test (hyp,_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if Term.eq_constr x y then None else match kind_of_term x, kind_of_term y with - | Var _, _ | _, Var _ -> Some hyp - | _ -> None + | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> + Some hyp + | _ -> + None with Constr_matching.PatternMatchingFailure -> None in let hyps = Proofview.Goal.hyps gl in @@ -1694,9 +1695,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else match kind_of_term x, kind_of_term y with - | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true) - | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false) - | _ -> Proofview.tclUNIT () + | Var x', _ when not (occur_term x y) -> + subst_one flags.rewrite_dependent_proof x' (hyp,y,true) + | _, Var y' when not (occur_term y x) -> + subst_one flags.rewrite_dependent_proof y' (hyp,x,false) + | _ -> + Proofview.tclUNIT () end in Proofview.Goal.nf_enter begin fun gl -> diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v new file mode 100644 index 0000000000..8336f6a806 --- /dev/null +++ b/test-suite/success/subst.v @@ -0,0 +1,25 @@ +(* Test various subtleties of the "subst" tactics *) + +(* Should proceed from left to right (see #4222) *) +Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y. +intros. +subst. +change (3 = 2) in H1. +change (3 = 3). +Abort. + +(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *) +Goal forall x y, x = y -> x = 3 -> x = y. +intros. +subst. +change (3 = 3). +Abort. + +(* Should substitute cycles once, until a recursive equation is obtained *) +(* (failed in 8.4) *) +Goal forall x y, x = S y -> y = S x -> x = y. +intros. +subst. +change (y = S (S y)) in H0. +change (S y = y). +Abort. -- cgit v1.2.3 From 3bcfff90470ef079b5e711ef72db28b670eeacd0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 8 May 2015 12:41:07 +0200 Subject: A more user-friendly naming of variables of ltac names defined by TACTIC EXTEND (based on user-given name). --- grammar/tacextend.ml4 | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 0421ad7ce4..f5f11e30a8 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -172,17 +172,17 @@ let is_constr_gram = function | Aentry ("constr", "constr") -> true | _ -> false -let make_vars len = - (** We choose names unlikely to be written by a human, even though that - does not matter at all. *) - List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i))) +let make_var = function + | GramNonTerminal(loc',_,_,Some p) -> Some p + | GramNonTerminal(loc',_,_,None) -> Some (Id.of_string "_") + | _ -> assert false let declare_tactic loc s c cl = match cl with | [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in - let vars = make_vars (List.length rem) in + let vars = List.map make_var rem in let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in -- cgit v1.2.3 From 5cbc018fe934750bdf1043da68f99911be4ee6f6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 5 May 2015 19:25:24 +0200 Subject: Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for preserving compatibility of subst after #4214 being solved. --- CHANGES | 10 +++++----- tactics/equality.ml | 37 +++++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/4214.v | 5 ----- test-suite/bugs/opened/4214.v | 5 +++++ 4 files changed, 47 insertions(+), 10 deletions(-) delete mode 100644 test-suite/bugs/closed/4214.v create mode 100644 test-suite/bugs/opened/4214.v diff --git a/CHANGES b/CHANGES index 87506dadc1..85a207c29f 100644 --- a/CHANGES +++ b/CHANGES @@ -5,6 +5,11 @@ Vernacular commands - New command "Redirect" to redirect the output of a command to a file. +Tactics + +- New flag "Set Regular Subst Tactic" which fixes "subst" in situations where + it failed to substitute all substitutable equations or failed to simplify + cycles, or accidentally unfolded local definitions (flag is off by default). Changes from V8.5beta1 to V8.5beta2 =================================== @@ -19,7 +24,6 @@ Tactics - A script using the admit tactic can no longer be concluded by either Qed or Defined. In the first case, Admitted can be used instead. In the second case, a subproof should be used. - - The easy tactic and the now tactical now have a more predictable behavior, but they might now discharge some previously unsolved goals. @@ -27,25 +31,21 @@ Extraction - Definitions extracted to Haskell GHC should no longer randomly segfault when some Coq types cannot be represented by Haskell types. - - Definitions can now be extracted to Json for post-processing. Tools - Option -I -as has been removed, and option -R -as has been deprecated. In both cases, option -R can be used instead. - - coq_makefile now generates double-colon rules for rules such as clean. API - The interface of [change] has changed to take a [change_arg], which can be built from a [constr] using [make_change_arg]. - - [pattern_of_constr] now returns a triplet including the cleaned-up [evar_map], removing the evars that were turned into metas. - Changes from V8.4 to V8.5beta1 ============================== diff --git a/tactics/equality.ml b/tactics/equality.ml index 591fbabaef..593b7e9ea0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1662,8 +1662,21 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } +let regular_subst_tactic = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "more regular behavior of tactic subst"; + optkey = ["Regular";"Subst";"Tactic"]; + optread = (fun () -> !regular_subst_tactic); + optwrite = (:=) regular_subst_tactic } + let subst_all ?(flags=default_subst_tactic_flags ()) () = + if !regular_subst_tactic then + (* First step: find hypotheses to treat in linear time *) let find_equations gl = let gl = Proofview.Goal.assume gl in @@ -1708,6 +1721,30 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = tclMAP process ids end + else + +(* Old implementation, not able to manage configurations like a=b, a=t, + or situations like "a = S b, b = S a", or also accidentally unfolding + let-ins *) + Proofview.Goal.nf_enter begin fun gl -> + let find_eq_data_decompose = find_eq_data_decompose gl in + let test (_,c) = + try + let lbeq,u,(_,x,y) = find_eq_data_decompose c in + let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + if flags.only_leibniz then restrict_to_eq_and_identity eq; + (* J.F.: added to prevent failure on goal containing x=x as an hyp *) + if Term.eq_constr x y then failwith "caught"; + match kind_of_term x with Var x -> x | _ -> + match kind_of_term y with Var y -> y | _ -> failwith "caught" + with Constr_matching.PatternMatchingFailure -> failwith "caught" in + let test p = try Some (test p) with Failure _ -> None in + let hyps = pf_hyps_types gl in + let ids = List.map_filter test hyps in + let ids = List.uniquize ids in + subst_gen flags.rewrite_dependent_proof ids + end + (* Rewrite the first assumption for which a condition holds and gives the direction of the rewrite *) diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v deleted file mode 100644 index cd53c898e9..0000000000 --- a/test-suite/bugs/closed/4214.v +++ /dev/null @@ -1,5 +0,0 @@ -(* Check that subst uses all equations around *) -Goal forall A (a b c : A), b = a -> b = c -> a = c. -intros. -subst. -reflexivity. diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v new file mode 100644 index 0000000000..cd53c898e9 --- /dev/null +++ b/test-suite/bugs/opened/4214.v @@ -0,0 +1,5 @@ +(* Check that subst uses all equations around *) +Goal forall A (a b c : A), b = a -> b = c -> a = c. +intros. +subst. +reflexivity. -- cgit v1.2.3 From 39a67d502d341562b68c0f52163b2863bdd5ebd4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 May 2015 18:04:40 +0200 Subject: Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default). --- test-suite/bugs/opened/4214.v | 2 +- test-suite/success/subst.v | 25 ------------------------- 2 files changed, 1 insertion(+), 26 deletions(-) delete mode 100644 test-suite/success/subst.v diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v index cd53c898e9..3daf452132 100644 --- a/test-suite/bugs/opened/4214.v +++ b/test-suite/bugs/opened/4214.v @@ -2,4 +2,4 @@ Goal forall A (a b c : A), b = a -> b = c -> a = c. intros. subst. -reflexivity. +Fail reflexivity. diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v deleted file mode 100644 index 8336f6a806..0000000000 --- a/test-suite/success/subst.v +++ /dev/null @@ -1,25 +0,0 @@ -(* Test various subtleties of the "subst" tactics *) - -(* Should proceed from left to right (see #4222) *) -Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y. -intros. -subst. -change (3 = 2) in H1. -change (3 = 3). -Abort. - -(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *) -Goal forall x y, x = y -> x = 3 -> x = y. -intros. -subst. -change (3 = 3). -Abort. - -(* Should substitute cycles once, until a recursive equation is obtained *) -(* (failed in 8.4) *) -Goal forall x y, x = S y -> y = S x -> x = y. -intros. -subst. -change (y = S (S y)) in H0. -change (S y = y). -Abort. -- cgit v1.2.3 From eef0ffe1646d09c81de23ad34f58a75d63a88372 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 10 May 2015 19:41:12 +0200 Subject: Code factorization in Constr_matching. --- pretyping/constr_matching.ml | 52 +++++++++++++++++--------------------------- 1 file changed, 20 insertions(+), 32 deletions(-) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index e281807131..5098665582 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -343,56 +343,49 @@ let matches_head env sigma pat c = matches env sigma pat head (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx next = +let authorized_occ env sigma partial_app closed pat c mk_ctx = try let subst = matches_core_closed env sigma false partial_app pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst) - then next () - else mkresult subst (mk_ctx (mkMeta special_meta)) next - with PatternMatchingFailure -> next () + then (fun next -> next ()) + else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) + with PatternMatchingFailure -> (fun next -> next ()) let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let rec aux env c mk_ctx next = - match kind_of_term c with + let here = authorized_occ env sigma partial_app closed pat c mk_ctx in + let next () = match kind_of_term c with | Cast (c1,k,c2) -> let next_mk_ctx = function | [c1] -> mk_ctx (mkCast (c1, k, c2)) | _ -> assert false in - let next () = try_aux [env, c1] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux [env, c1] next_mk_ctx next | Lambda (x,c1,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2)) | _ -> assert false in - let next () = - let env' = Environ.push_rel (x,None,c1) env in - try_aux [(env, c1); (env', c2)] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + let env' = Environ.push_rel (x,None,c1) env in + try_aux [(env, c1); (env', c2)] next_mk_ctx next | Prod (x,c1,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkProd (x, c1, c2)) | _ -> assert false in - let next () = - let env' = Environ.push_rel (x,None,c1) env in - try_aux [(env, c1); (env', c2)] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + let env' = Environ.push_rel (x,None,c1) env in + try_aux [(env, c1); (env', c2)] next_mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2)) | _ -> assert false in - let next () = - let env' = Environ.push_rel (x,Some c1,t) env in - try_aux [(env, c1); (env', c2)] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + let env' = Environ.push_rel (x,Some c1,t) env in + try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> - let next () = let topdown = true in if partial_app then if topdown then @@ -421,45 +414,40 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in let sub = (env, c1) :: subargs env lc in try_aux sub mk_ctx next - in - authorized_occ env sigma partial_app closed pat c mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in let sub = (env, hd) :: (env, c1) :: subargs env lc in - let next () = try_aux sub next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in let sub = subargs env types @ subargs env bodies in - let next () = try_aux sub next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux sub next_mk_ctx next | CoFix (i,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in let sub = subargs env types @ subargs env bodies in - let next () = try_aux sub next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux sub next_mk_ctx next | Proj (p,c') -> let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - let next () = if partial_app then try let term = Retyping.expand_projection env sigma p c' [] in aux env term mk_ctx next with Retyping.RetypeError _ -> next () else - try_aux [env, c'] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux [env, c'] next_mk_ctx next | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - authorized_occ env sigma partial_app closed pat c mk_ctx next + next () + in + here next (* Tries [sub_match] for all terms in the list *) and try_aux lc mk_ctx next = -- cgit v1.2.3 From 9a883e3740e21c93c8ea7f51b0cf0c4a76675773 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 May 2015 08:34:50 +0200 Subject: Rationalizing a bit the interface of Hints. --- plugins/firstorder/sequent.ml | 2 +- tactics/auto.ml | 2 +- tactics/auto.mli | 2 +- tactics/class_tactics.ml | 8 ++++---- tactics/eauto.ml4 | 4 ++-- tactics/hints.ml | 28 ++++++++++++++-------------- tactics/hints.mli | 28 ++++++++++++++-------------- 7 files changed, 37 insertions(+), 37 deletions(-) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7d034db552..802af04d06 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -209,7 +209,7 @@ open Hints let extend_with_auto_hints l seq gl= let seqref=ref seq in let f p_a_t = - match repr_auto_tactic p_a_t.code with + match repr_hint p_a_t.code with Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> (try diff --git a/tactics/auto.ml b/tactics/auto.ml index 7da8415714..72ba9e0bd9 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -377,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Extern tacast -> conclPattern concl p tacast in - tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic) + tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic) and trivial_resolve dbg mod_delta db_list local_db cl = try diff --git a/tactics/auto.mli b/tactics/auto.mli index 0cc8a0b1b9..8dacc13629 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -19,7 +19,7 @@ val extern_interp : (** Auto and related automation tactics *) -val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list +val priority : ('a * full_hint) list -> ('a * full_hint) list val default_search_depth : int ref diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e11458c049..6ea25269cf 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -231,13 +231,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl = | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) | Extern tacast -> conclPattern concl p tacast in - let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in + let tac = Proofview.V82.of_tactic (run_hint t tac) in let tac = if complete then tclCOMPLETE tac else tac in - match repr_auto_tactic t with - | Extern _ -> (tac,b,true, name, lazy (pr_autotactic t)) + match repr_hint t with + | Extern _ -> (tac,b,true, name, lazy (pr_hint t)) | _ -> (* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) - (tac,b,false, name, lazy (pr_autotactic t)) + (tac,b,false, name, lazy (pr_hint t)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db sigma concl = diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index d738677e50..50925ecde6 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -172,8 +172,8 @@ and e_my_find_search db_list local_db hdc concl = | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) | Extern tacast -> conclPattern concl p tacast in - let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in - (tac, lazy (pr_autotactic t))) + let tac = Proofview.V82.of_tactic (run_hint t tac) in + (tac, lazy (pr_hint t))) in List.map tac_of_hint hintl diff --git a/tactics/hints.ml b/tactics/hints.ml index f83aa56017..b8e4dd9fa4 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -68,7 +68,7 @@ let decompose_app_bound t = (* The Type of Constructions Autotactic Hints *) (************************************************************************) -type 'a auto_tactic_ast = +type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -92,9 +92,9 @@ type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set -type 'a auto_tactic = 'a auto_tactic_ast +type hint = (constr * clausenv) hint_ast -type 'a gen_auto_tactic = { +type 'a with_metadata = { pri : int; (* A number lower is higher priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (* A pattern for the concl of the Goal *) @@ -102,13 +102,13 @@ type 'a gen_auto_tactic = { code : 'a (* the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic +type full_hint = hint with_metadata type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic + (constr * types * Univ.universe_context_set) hint_ast with_metadata -let run_auto_tactic tac k = k tac -let repr_auto_tactic tac = tac +let run_hint tac k = k tac +let repr_hint h = h let eq_hints_path_atom p1 p2 = match p1, p2 with | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2 @@ -125,7 +125,7 @@ let eq_auto_tactic t1 t2 = match t1, t2 with | (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _ | Unfold_nth _ | Extern _), _ -> false -let eq_gen_auto_tactic t1 t2 = +let eq_hint_metadata t1 t2 = Int.equal t1.pri t2.pri && Option.equal constr_pattern_eq t1.pat t2.pat && eq_hints_path_atom t1.name t2.name && @@ -153,7 +153,7 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0 - un discrimination net borné (Btermdn.t) constitué de tous les patterns de la seconde liste de tactiques *) -type stored_data = int * pri_auto_tactic +type stored_data = int * full_hint (* First component is the index of insertion in the table, to keep most recent first semantics. *) module Bounded_net = Btermdn.Make(struct @@ -481,7 +481,7 @@ module Hint_db = struct match k with | None -> (** ppedrot: this equality here is dubious. Maybe we can remove it? *) - let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in + let is_present (_, (_, v')) = eq_hint_metadata v v' in if not (List.exists is_present db.hintdb_nopat) then (** FIXME *) { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } @@ -1146,7 +1146,7 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_autotactic = +let pr_hint = function | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c) | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c) @@ -1163,11 +1163,11 @@ let pr_autotactic = in (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) -let pr_hint (id, v) = - (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) +let pr_id_hint (id, v) = + (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) let pr_hint_list hintlist = - (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ()) + (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) let pr_hints_db (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ diff --git a/tactics/hints.mli b/tactics/hints.mli index 958cca1c3b..687bc78c76 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array (** Pre-created hint databases *) -type 'a auto_tactic_ast = +type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -36,13 +36,13 @@ type 'a auto_tactic_ast = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) -type 'a auto_tactic +type hint type hints_path_atom = | PathHints of global_reference list | PathAny -type 'a gen_auto_tactic = private { +type 'a with_metadata = private { pri : int; (** A number between 0 and 4, 4 = lower priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) @@ -50,7 +50,7 @@ type 'a gen_auto_tactic = private { code : 'a; (** the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic +type full_hint = hint with_metadata type search_entry @@ -76,28 +76,28 @@ module Hint_db : type t val empty : transparent_state -> bool -> t val find : global_reference -> t -> search_entry - val map_none : t -> pri_auto_tactic list + val map_none : t -> full_hint list (** All hints associated to the reference *) - val map_all : global_reference -> t -> pri_auto_tactic list + val map_all : global_reference -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) - val map_existential : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) - val map_auto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list val add_one : hint_entry -> t -> t val add_list : (hint_entry) list -> t -> t val remove_one : global_reference -> t -> t val remove_list : global_reference list -> t -> t - val iter : (global_reference option -> bool array list -> pri_auto_tactic list -> unit) -> t -> unit + val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state @@ -197,12 +197,12 @@ val make_extern : int -> constr_pattern option -> Tacexpr.glob_tactic_expr -> hint_entry -val run_auto_tactic : 'a auto_tactic -> - ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic +val run_hint : hint -> + ((constr * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic (** This function is for backward compatibility only, not to use in newly written code. *) -val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast +val repr_hint : hint -> (constr * clausenv) hint_ast val extern_intern_tac : (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t @@ -227,7 +227,7 @@ val pr_applicable_hint : unit -> std_ppcmds val pr_hint_ref : global_reference -> std_ppcmds val pr_hint_db_by_name : hint_db_name -> std_ppcmds val pr_hint_db : Hint_db.t -> std_ppcmds -val pr_autotactic : (constr * 'a) auto_tactic -> Pp.std_ppcmds +val pr_hint : hint -> Pp.std_ppcmds (** Hook for changing the initialization of auto *) -- cgit v1.2.3 From 138bd9756a0fc80647427b2894ba4485f3e6961b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 May 2015 11:06:32 +0200 Subject: Fixing bug #4232. We beta-iota normalize the type of the rewriting predicate to ensure that the non-dependency in the arrow argument is meaningful. Otherwise, terms of the form "forall x : A, (fun _ : A => P) x" generated by the retyping would confuse the non-dependency heuristic. --- tactics/rewrite.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 1be394aa4a..d487317736 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -226,6 +226,7 @@ end) = struct let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in match kind_of_term t, l with | Prod (na, ty, b), obj :: cstrs -> + let b = Reductionops.nf_betaiota (goalevars evars) b in if noccurn 1 b (* non-dependent product *) then let ty = Reductionops.nf_betaiota (goalevars evars) ty in let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in -- cgit v1.2.3 From 7bc1610376fac29397be39d4a06b178e8e35e66e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 May 2015 11:17:54 +0200 Subject: Test for bug #4232. --- test-suite/bugs/closed/4232.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 test-suite/bugs/closed/4232.v diff --git a/test-suite/bugs/closed/4232.v b/test-suite/bugs/closed/4232.v new file mode 100644 index 0000000000..61e544a914 --- /dev/null +++ b/test-suite/bugs/closed/4232.v @@ -0,0 +1,20 @@ +Require Import Setoid Morphisms Vector. + +Class Equiv A := equiv : A -> A -> Prop. +Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv). + +Global Declare Instance vec_equiv {A} `{Equiv A} {n}: Equiv (Vector.t A n). +Global Declare Instance vec_setoid A `{Setoid A} n : Setoid (Vector.t A n). + +Global Declare Instance tl_proper1 {A} `{Equiv A} n: + Proper ((equiv) ==> (equiv)) + (@tl A n). + +Lemma test: + forall {A} `{Setoid A} n (xa ya: Vector.t A (S n)), + (equiv xa ya) -> equiv (tl xa) (tl ya). +Proof. + intros A R HA n xa ya Heq. + setoid_rewrite Heq. + reflexivity. +Qed. -- cgit v1.2.3 From 2a2d418971a019202cdb78fabc7658a543f0886d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 May 2015 18:18:07 +0200 Subject: Adding a test to check whether two tactic notations conflict. --- tactics/tacenv.ml | 2 ++ tactics/tacenv.mli | 3 +++ toplevel/metasyntax.ml | 7 +++++++ 3 files changed, 12 insertions(+) diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index ffff44d5bc..08e8bc0112 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -26,6 +26,8 @@ let interp_alias key = try KNmap.find key !alias_map with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) +let check_alias key = KNmap.mem key !alias_map + (** ML tactic extensions (TacML) *) type ml_tactic = diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4ca..9410ccb389 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -23,6 +23,9 @@ val register_alias : alias -> glob_tactic_expr -> unit val interp_alias : alias -> glob_tactic_expr (** Recover the the body of an alias. Raises an anomaly if it does not exist. *) +val check_alias : alias -> bool +(** Returns [true] if an alias is defined, false otherwise. *) + (** {5 Coq tactic definitions} *) val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index f4fabc4d3a..300bf5b490 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -84,8 +84,14 @@ type tactic_grammar_obj = { tacobj_body : Tacexpr.glob_tactic_expr } +let check_key key = + if Tacenv.check_alias key then + error "Conflicting tactic notations keys. This can happen when including \ + twice the same module." + let cache_tactic_notation (_, tobj) = let key = tobj.tacobj_key in + let () = check_key key in Tacenv.register_alias key tobj.tacobj_body; Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp @@ -97,6 +103,7 @@ let open_tactic_notation i (_, tobj) = let load_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in + let () = check_key key in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; -- cgit v1.2.3 From 0803c2dd715e6493c3e4f865bcf9ca2a16318c55 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 12 May 2015 07:46:15 +0200 Subject: STM: process_error_hook set in Vernac where fname is known (fix #4229) In compiler mode, only vernac.ml knows the current file name. Stm.process_error_hook moved from Vernacentries to Vernac to be bale to properly enrich the exception with the current file name (if any). --- toplevel/vernac.ml | 19 ++++++++++++++----- toplevel/vernacentries.ml | 1 - 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 11cb047e09..96daf5075d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -78,9 +78,13 @@ let get_exn_files e = Exninfo.get e files_of_exn let add_exn_files e f = Exninfo.add e files_of_exn f -let raise_with_file f (e, info) = - let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in - iraise (e, add_exn_files info { outer = f; inner = inner_f }) +let enrich_with_file f (e, info) = + let inner = match get_exn_files info with None -> f | Some x -> x.inner in + (e, add_exn_files info { outer = f; inner }) + +let raise_with_file f e = iraise (enrich_with_file f e) + +let cur_file = ref None let disable_drop = function | Drop -> Errors.error "Drop is forbidden." @@ -258,8 +262,8 @@ and read_vernac_file verbosely s = if is_navigation_vernac cmd && not (is_reset cmd) then user_error loc "Navigation commands forbidden in files" in - let (in_chan, fname, input) = - open_file_twice_if verbosely s in + let (in_chan, fname, input) = open_file_twice_if verbosely s in + cur_file := Some fname; try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) @@ -350,3 +354,8 @@ let compile v f = compile v f; CoqworkmgrApi.giveback 1 +let () = Hook.set Stm.process_error_hook (fun e -> + match !cur_file with + | None -> Cerrors.process_vernac_interp_error e + | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e) +) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4300d5e244..6272625bda 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2164,5 +2164,4 @@ let interp ?(verbosely=true) ?proof (loc,c) = else aux false c let () = Hook.set Stm.interp_hook interp -let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error let () = Hook.set Stm.with_fail_hook with_fail -- cgit v1.2.3 From 17f2b11a9a6bb39379239122e77ec12d0b96ff63 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 12 May 2015 14:19:13 +0200 Subject: nice error for Restart outside a proof (Close: #4235) --- stm/stm.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index 9771564752..97903e721b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -846,7 +846,8 @@ end = struct (* {{{ *) | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup") | Some vcs, _ -> vcs in let cb, _ = - Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in + try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) + with Failure _ -> raise Proof_global.NoCurrentProof in let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in -- cgit v1.2.3 From a49cd60c67aca452500c82aad61327823f9abe31 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 12 May 2015 14:16:19 +0200 Subject: Fixing bug #4234. --- pretyping/evarutil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 2508f4ef3b..6d076ecd11 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -713,7 +713,7 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = whd_evar evd evi.evar_concl in + let concl = whd_betadeltaiota evenv evd evi.evar_concl in let s = destSort concl in let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = -- cgit v1.2.3 From 20fd4f91c5096d2f9c06f2bdca23127be4d81aad Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 12 May 2015 14:17:45 +0200 Subject: Test for bug #4234. --- test-suite/bugs/closed/4234.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/closed/4234.v diff --git a/test-suite/bugs/closed/4234.v b/test-suite/bugs/closed/4234.v new file mode 100644 index 0000000000..348dd49d93 --- /dev/null +++ b/test-suite/bugs/closed/4234.v @@ -0,0 +1,7 @@ +Definition UU := Type. + +Definition dirprodpair {X Y : UU} := existT (fun x : X => Y). + +Definition funtoprodtoprod {X Y Z : UU} : { a : X -> Y & X -> Z }. +Proof. + refine (dirprodpair _ (fun x => _)). -- cgit v1.2.3 From 95b4a54ec6a9aacffe8c11df1b443d36b9f6dda7 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 May 2015 16:48:01 +0200 Subject: Extraction: fix the detection of the "polyprop" situation The ~polyprop argument wasn't propagated properly anymore, leading the extraction to try to operate on situations it cannot handle (yet). Cf Table.error_singleton_become_prop for more details. Regression test added. --- kernel/inductive.ml | 2 +- test-suite/success/extraction_polyprop.v | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test-suite/success/extraction_polyprop.v diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca814f497c..088b99b9e0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -214,7 +214,7 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a (ty, cst) let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = - type_of_inductive_gen env mip args + type_of_inductive_gen ~polyprop env mip args (* The max of an array of universes *) diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v new file mode 100644 index 0000000000..7215bd9905 --- /dev/null +++ b/test-suite/success/extraction_polyprop.v @@ -0,0 +1,11 @@ +(* The current extraction cannot handle this situation, + and shouldn't try, otherwise it might produce some Ocaml + code that segfaults. See Table.error_singleton_become_prop + or S. Glondu's thesis for more details. *) + +Definition f {X} (p : (nat -> X) * True) : X * nat := + (fst p 0, 0). + +Definition f_prop := f ((fun _ => I),I). + +Fail Extraction f_prop. -- cgit v1.2.3 From 19752ec7e7ec2a89e01c9c65b1cc472cca04e424 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 Apr 2015 14:17:31 +0200 Subject: Adding unique identifiers to hints. --- tactics/hints.ml | 101 ++++++++++++++++++++++++++++++------------------------- 1 file changed, 55 insertions(+), 46 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index b8e4dd9fa4..5a5be1cbc5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -92,23 +92,43 @@ type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set -type hint = (constr * clausenv) hint_ast +type 'a with_uid = { + obj : 'a; + uid : KerName.t; +} + +type hint = (constr * clausenv) hint_ast with_uid type 'a with_metadata = { pri : int; (* A number lower is higher priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (* A pattern for the concl of the Goal *) name : hints_path_atom; (* A potential name to refer to the hint *) - code : 'a (* the tactic to apply when the concl matches pat *) + code : 'a; (* the tactic to apply when the concl matches pat *) } type full_hint = hint with_metadata type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) hint_ast with_metadata - -let run_hint tac k = k tac -let repr_hint h = h + (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata + +let run_hint tac k = k tac.obj +let repr_hint h = h.obj + +let fresh_key = + let id = Summary.ref ~name:"HINT-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) let eq_hints_path_atom p1 p2 = match p1, p2 with | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2 @@ -175,21 +195,7 @@ let empty_se = { sentry_mode = []; } -let eq_pri_auto_tactic (_, x) (_, y) = - if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then - match x.code,y.code with - | Res_pf (cstr,_),Res_pf (cstr1,_) -> - Term.eq_constr cstr cstr1 - | ERes_pf (cstr,_),ERes_pf (cstr1,_) -> - Term.eq_constr cstr cstr1 - | Give_exact (cstr,_),Give_exact (cstr1,_) -> - Term.eq_constr cstr cstr1 - | Res_pf_THEN_trivial_fail (cstr,_) - ,Res_pf_THEN_trivial_fail (cstr1,_) -> - Term.eq_constr cstr cstr1 - | _,_ -> false - else - false +let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid let add_tac pat t st se = match pat with @@ -248,7 +254,7 @@ let instantiate_hint p = { cl.templval with rebus = strip_params env cl.templval.rebus }; env = empty_env} in - let code = match p.code with + let code = match p.code.obj with | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx) | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx) | Res_pf_THEN_trivial_fail (c, cty, ctx) -> @@ -256,7 +262,8 @@ let instantiate_hint p = | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx) | Unfold_nth e -> Unfold_nth e | Extern t -> Extern t - in { pri = p.pri; poly = p.poly; name = p.name; pat = p.pat; code = code } + in + { p with code = { p.code with obj = code } } let hints_path_atom_eq h1 h2 = match h1, h2 with | PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2 @@ -473,15 +480,14 @@ module Hint_db = struct let idv = id, v in let k = match gr with | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && - is_unfold v.code then None else Some gr + is_unfold v.code.obj then None else Some gr | None -> None in let dnst = if db.use_dn then Some db.hintdb_state else None in - let pat = if not db.use_dn && is_exact v.code then None else v.pat in + let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in match k with | None -> - (** ppedrot: this equality here is dubious. Maybe we can remove it? *) - let is_present (_, (_, v')) = eq_hint_metadata v v' in + let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in if not (List.exists is_present db.hintdb_nopat) then (** FIXME *) { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } @@ -500,7 +506,7 @@ module Hint_db = struct let add_one (k, v) db = let v = instantiate_hint v in let st',db,rebuild = - match v.code with + match v.code.obj with | Unfold_nth egr -> let addunf (ids,csts) (ids',csts') = match egr with @@ -632,6 +638,8 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable." +let with_uid c = { obj = c; uid = fresh_key () } + let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = let cty = strip_outer_cast cty in match kind_of_term cty with @@ -647,7 +655,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = poly = poly; pat = Some pat; name = name; - code = Give_exact (c, cty, ctx) }) + code = with_uid (Give_exact (c, cty, ctx)); }) let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in @@ -667,7 +675,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; - code = Res_pf(c,cty,ctx) }) + code = with_uid (Res_pf(c,cty,ctx)); }) else begin if not eapply then failwith "make_apply_entry"; if verbose then @@ -678,7 +686,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; - code = ERes_pf(c,cty,ctx) }) + code = with_uid (ERes_pf(c,cty,ctx)); }) end | _ -> failwith "make_apply_entry" @@ -724,7 +732,7 @@ let make_unfold eref = poly = false; pat = None; name = PathHints [g]; - code = Unfold_nth eref }) + code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = let hdconstr = Option.map try_head_pattern pat in @@ -733,7 +741,7 @@ let make_extern pri pat tacast = poly = false; pat = pat; name = PathAny; - code = Extern tacast }) + code = with_uid (Extern tacast) }) let make_mode ref m = let ty = Global.type_of_global_unsafe ref in @@ -756,7 +764,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = poly = poly; pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); name = name; - code=Res_pf_THEN_trivial_fail(c,t,ctx) }) + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -771,7 +779,7 @@ let get_db dbname = try searchtable_map dbname with Not_found -> Hint_db.empty empty_transparent_state false -let add_hint dbname hintlist = +let add_hint dbname hintlist = let db = get_db dbname in let db' = Hint_db.add_list hintlist db in searchtable_add (dbname,db') @@ -837,34 +845,36 @@ let subst_autohint (subst, obj) = let subst_hint (k,data as hint) = let k' = Option.smartmap subst_key k in let pat' = Option.smartmap (subst_pattern subst) data.pat in - let code' = match data.code with + let code' = match data.code.obj with | Res_pf (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'==t then data.code else Res_pf (c', t',ctx) + if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx) | ERes_pf (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'==t then data.code else ERes_pf (c',t',ctx) + if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx) | Give_exact (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'== t then data.code else Give_exact (c',t',ctx) + if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx) | Res_pf_THEN_trivial_fail (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t',ctx) + if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx) | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in - if ref==ref' then data.code else Unfold_nth ref' + if ref==ref' then data.code.obj else Unfold_nth ref' | Extern tac -> let tac' = Tacsubst.subst_tactic subst tac in - if tac==tac' then data.code else Extern tac' + if tac==tac' then data.code.obj else Extern tac' in let name' = subst_path_atom subst data.name in + let uid' = subst_kn subst data.code.uid in let data' = - if data.pat==pat' && data.name == name' && data.code==code' then data - else { data with pat = pat'; name = name'; code = code' } + if data.code.uid == uid' && data.pat == pat' && + data.name == name' && data.code.obj == code' then data + else { data with pat = pat'; name = name'; code = { obj = code'; uid = uid' } } in if k' == k && data' == data then hint else (k',data') in @@ -1146,8 +1156,7 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_hint = - function +let pr_hint h = match h.obj with | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c) | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c) | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c) -- cgit v1.2.3 From e0a245daa30a3204ee487fe6f8d20a0674a2398c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 May 2015 18:34:00 +0200 Subject: Adding an option Loose Hint Behavior to handle hints loaded but not imported. It accepts three distinct flags: - "Lax", which is the default one, sets the old behaviour, i.e. a non-imported hint behaves the same as an imported one. - "Warn" outputs a warning when a non-imported hint is used. Note that this is an over-approximation, because a hint may be triggered by an eauto run that will eventually fail and backtrack. - "Strict" changes the behaviour of an unloaded hint to the one of the fail tactic, allowing to emulate the hopefully future import-scoped hint mechanism. --- tactics/hints.ml | 80 +++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 73 insertions(+), 7 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index 5a5be1cbc5..ae45aabd0b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -112,8 +112,29 @@ type full_hint = hint with_metadata type hint_entry = global_reference option * (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata -let run_hint tac k = k tac.obj -let repr_hint h = h.obj +type import_level = [ `LAX | `WARN | `STRICT ] + +let warn_hint : import_level ref = ref `LAX +let read_warn_hint () = match !warn_hint with +| `LAX -> "Lax" +| `WARN -> "Warn" +| `STRICT -> "Strict" + +let write_warn_hint = function +| "Lax" -> warn_hint := `LAX +| "Warn" -> warn_hint := `WARN +| "Strict" -> warn_hint := `STRICT +| _ -> error "Only the following flags are accepted: Lax, Warn, Strict." + +let _ = + Goptions.declare_string_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "behavior of non-imported hints"; + Goptions.optkey = ["Loose"; "Hint"; "Behavior"]; + Goptions.optread = read_warn_hint; + Goptions.optwrite = write_warn_hint; + } let fresh_key = let id = Summary.ref ~name:"HINT-COUNTER" 0 in @@ -592,6 +613,7 @@ let auto_init_db = Hintdbmap.empty) let searchtable : hint_db_table = ref auto_init_db +let statustable = ref KNmap.empty let searchtable_map name = Hintdbmap.find name !searchtable @@ -615,9 +637,10 @@ let add_hints_init f = let init = !hints_init in hints_init := (fun () -> init (); f ()) -let init () = searchtable := auto_init_db; !hints_init () -let freeze _ = !searchtable -let unfreeze fs = searchtable := fs +let init () = + searchtable := auto_init_db; statustable := KNmap.empty; !hints_init () +let freeze _ = (!searchtable, !statustable) +let unfreeze (fs, st) = searchtable := fs; statustable := st let _ = Summary.declare_summary "search" { Summary.freeze_function = freeze; @@ -780,6 +803,14 @@ let get_db dbname = with Not_found -> Hint_db.empty empty_transparent_state false let add_hint dbname hintlist = + let check (_, h) = + let () = if KNmap.mem h.code.uid !statustable then + error "Conflicting hint keys. This can happen when including \ + twice the same module." + in + statustable := KNmap.add h.code.uid false !statustable + in + let () = List.iter check hintlist in let db = get_db dbname in let db' = Hint_db.add_list hintlist db in searchtable_add (dbname,db') @@ -824,7 +855,7 @@ type hint_obj = { hint_action : hint_action; } -let cache_autohint (_, h) = +let load_autohint _ (kn, h) = let name = h.hint_name in match h.hint_action with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) @@ -834,6 +865,16 @@ let cache_autohint (_, h) = | AddCut path -> add_cut name path | AddMode (l, m) -> add_mode name l m +let open_autohint i (kn, h) = + if Int.equal i 1 then match h.hint_action with + | AddHints hints -> + let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in + List.iter add hints + | _ -> () + +let cache_autohint (kn, obj) = + load_autohint 1 (kn, obj); open_autohint 1 (kn, obj) + let subst_autohint (subst, obj) = let subst_key gr = let (lab'', elab') = subst_global subst gr in @@ -906,7 +947,8 @@ let classify_autohint obj = let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; - load_function = (fun _ -> cache_autohint); + load_function = load_autohint; + open_function = open_autohint; subst_function = subst_autohint; classify_function = classify_autohint; } @@ -1275,3 +1317,27 @@ let pr_searchtable () = in Hintdbmap.fold fold !searchtable (mt ()) +let print_mp mp = + try + let qid = Nametab.shortest_qualid_of_module mp in + str " from " ++ pr_qualid qid + with Not_found -> mt () + +let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true + +let warn h x = + let hint = pr_hint h in + let (mp, _, _) = KerName.repr h.uid in + let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in + Proofview.tclUNIT x + +let run_hint tac k = match !warn_hint with +| `LAX -> k tac.obj +| `WARN -> + if is_imported tac then k tac.obj + else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x) +| `STRICT -> + if is_imported tac then k tac.obj + else Proofview.tclZERO (UserError ("", (str "Tactic failure."))) + +let repr_hint h = h.obj -- cgit v1.2.3 From f480f07c232b4bcc4ea67bf0577e267d0fdc35f4 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 May 2015 17:22:09 +0200 Subject: Fix my previous commit on ~polyprop Oups, sorry, I should have compiled the stdlib in full. Not only the ~polyprop wasn't propagated properly, but Matthieu made it be false by default somewhere instead of true. Argl... --- kernel/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 088b99b9e0..4c1614bac1 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -213,7 +213,7 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a let cst = instantiate_inductive_constraints mib u in (ty, cst) -let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = +let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = type_of_inductive_gen ~polyprop env mip args (* The max of an array of universes *) -- cgit v1.2.3 From 1f3ea50258490ac8b5a395ac0ff2bca7326e755f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 12 May 2015 17:55:10 +0200 Subject: Mark PreOrder as a consequence of Equivalence. (Fix bug #4213) --- theories/Classes/RelationClasses.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1a40e5d599..15cb02d37f 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -89,6 +89,11 @@ Section Defs. Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 := { }. + (** An Equivalence is a PreOrder plus symmetry. *) + + Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 := + { }. + (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) := -- cgit v1.2.3 From b338af912c32ab87d6668923add72a56408bddf8 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 May 2015 17:41:45 +0200 Subject: List.nth_error directly produces Some/None instead of value/error List.nth_error and List.hd_error were the only remaining places in the whole stdlib to use type "Exc" instead of "option" directly. So let's simplify things and use option everywhere. In particular, during teaching sessions about lists, we won't have anymore to explain the (lack of) difference between Exc,value,error and option,Some,None. This might cause a few incompatibilities in proof scripts, if they syntactically expect "value" or "error" to occur, but this should hopefully be very rare and quite easy to fix. --- theories/Lists/List.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 5819fbe5ef..e0e5d94d82 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -45,8 +45,8 @@ Section Lists. Definition hd_error (l:list A) := match l with - | [] => error - | x :: _ => value x + | [] => None + | x :: _ => Some x end. Definition tl (l:list A) := @@ -393,11 +393,11 @@ Section Elts. simpl; auto. Qed. - Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A := + Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A := match n, l with - | O, x :: _ => value x + | O, x :: _ => Some x | S n, _ :: l => nth_error l n - | _, _ => error + | _, _ => None end. Definition nth_default (default:A) (l:list A) (n:nat) : A := -- cgit v1.2.3 From d17090cee488844fddc444fdba4fd195c27707c7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 12 May 2015 17:32:38 +0200 Subject: Documenting the Loose Hint Behavior flag. --- CHANGES | 11 ++++++++++- doc/refman/RefMan-tac.tex | 43 +++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 51 insertions(+), 3 deletions(-) diff --git a/CHANGES b/CHANGES index 85a207c29f..cb77c297dd 100644 --- a/CHANGES +++ b/CHANGES @@ -7,9 +7,18 @@ Vernacular commands Tactics -- New flag "Set Regular Subst Tactic" which fixes "subst" in situations where +- New flag "Regular Subst Tactic" which fixes "subst" in situations where it failed to substitute all substitutable equations or failed to simplify cycles, or accidentally unfolded local definitions (flag is off by default). +- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a + special way. It accepts three distinct flags: + * "Lax", which is the default one, sets the old behavior, i.e. a non-imported + hint behaves the same as an imported one. + * "Warn" outputs a warning when a non-imported hint is used. Note that this is + an over-approximation, because a hint may be triggered by an eauto run that + will eventually fail and backtrack. + * "Strict" changes the behavior of an unloaded hint to the one of the fail + tactic, allowing to emulate the hopefully future import-scoped hint mechanism. Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2eebac18e6..d1e9ec7960 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3853,6 +3853,7 @@ development. \subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$ \mbox{\dots} \ident$_m$} +\label{RemoveHints} \comindex{Remove Hints} This command removes the hints associated to terms \term$_1$ \mbox{\dots} @@ -3931,8 +3932,9 @@ main subgoal excluded. \end{Variants} -\subsection{Hints and sections -\label{Hint-and-Section}} +\subsection{Hint locality +\label{Hint-Locality}} +\optindex{Loose Hint Behavior} Hints provided by the \texttt{Hint} commands are erased when closing a section. Conversely, all hints of a module \texttt{A} that are not @@ -3940,6 +3942,43 @@ defined inside a section (and not defined with option {\tt Local}) become available when the module {\tt A} is imported (using e.g. \texttt{Require Import A.}). +As of today, hints only have a binary behavior regarding locality, as described +above: either they disappear at the end of a section scope, or they remain +global forever. This causes a scalability issue, because hints coming from an +unrelated part of the code may badly influence another development. It can be +mitigated to some extent thanks to the {\tt Remove Hints} command +(see ~\ref{RemoveHints}), but this is a mere workaround and has some +limitations (for instance, external hints cannot be removed). + +A proper way to fix this issue is to bind the hints to their module scope, as +for most of the other objects Coq uses. Hints should only made available when +the module they are defined in is imported, not just required. It is very +difficult to change the historical behavior, as it would break a lot of scripts. +We propose a smooth transitional path by providing the {\tt Loose Hint Behavior} +option which accepts three flags allowing for a fine-grained handling of +non-imported hints. + +\begin{Variants} + +\item {\tt Set Loose Hint Behavior "Lax"} + + This is the default, and corresponds to the historical behavior, that is, + hints defined outside of a section have a global scope. + +\item {\tt Set Loose Hint Behavior "Warn"} + + When set, it outputs a warning when a non-imported hint is used. Note that + this is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being actually + useful for the proof. + +\item {\tt Set Loose Hint Behavior "Strict"} + + When set, it changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. + +\end{Variants} + \subsection{Setting implicit automation tactics} \subsubsection{\tt Proof with {\tac}} -- cgit v1.2.3 From 574b4096517b4ac9189c2226e1cd75745e788db0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 May 2015 09:11:22 +0200 Subject: Better fixing #4198 such that the term to match is looked for before the predicate, thus respecting the visual left-to-right top-down order (see a45bd5981092). This fixes CFGV. --- pretyping/constr_matching.ml | 2 +- test-suite/bugs/closed/4198.v | 24 ++++++++++++++++++++++++ 2 files changed, 25 insertions(+), 1 deletion(-) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 5098665582..a0493777a5 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -419,7 +419,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let sub = (env, hd) :: (env, c1) :: subargs env lc in + let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index ef991365d5..f85a60264d 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -1,3 +1,5 @@ +(* Check that the subterms of the predicate of a match are taken into account *) + Require Import List. Open Scope list_scope. Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), @@ -11,3 +13,25 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), match goal with | [ |- appcontext G[@hd] ] => idtac end. + +(* This second example comes from CFGV where inspecting subterms of a + match is expecting to inspect first the term to match (even though + it would certainly be better to provide a "match x with _ end" + construct for generically matching a "match") *) + +Ltac find_head_of_head_match T := + match T with context [?E] => + match T with + | E => fail 1 + | _ => constr:(E) + end + end. + +Ltac mydestruct := + match goal with + | |- ?T1 = _ => let E := find_head_of_head_match T1 in destruct E + end. + +Goal forall x, match x with 0 => 0 | _ => 0 end = 0. +intros. +mydestruct. -- cgit v1.2.3 From c5d9f483a48265941720afafd5952a917d80204b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 May 2015 10:31:22 +0200 Subject: Documenting Set Regular Subst Tactic (though unsure this is worth the level of details, and this option should certainly disappear eventually). --- doc/refman/RefMan-tac.tex | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d1e9ec7960..be82eaa018 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2803,6 +2803,7 @@ This tactic is deprecated. It can be replaced by {\tt enough} \subsection{\tt subst \ident} \tacindex{subst} +\optindex{Regular Subst Tactic} This tactic applies to a goal that has \ident\ in its context and (at least) one hypothesis, say {\tt H}, of type {\tt @@ -2822,6 +2823,26 @@ When several hypotheses have the form {\tt \ident=t} or {\tt Applies {\tt subst} repeatedly to all identifiers from the context for which an equality exists. + +\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set + Regular Subst Tactic}. When this option is activated, {\tt subst} + manages the following corner cases which otherwise it + does not: +\begin{itemize} +\item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$} + and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a + variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$} + or {\tt $u$ = \ident$_2$} +\item A context with cyclic dependencies as with hypotheses {\tt + \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} +\end{itemize} +Additionally, it prevents a local definition such as {\tt \ident := + $t$} to be unfolded which otherwise it would exceptionally unfold in +configurations containing hypotheses of the form {\tt {\ident} = $u$}, +or {\tt $u'$ = \ident} with $u'$ not a variable. + +The option is off by default. + \end{Variants} \subsection{\tt stepl \term} -- cgit v1.2.3 From f86b7d3b8cb23e2fc19a936accb421bfdbf2cb4d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2015 12:54:07 +0200 Subject: Fix for a second avatar of bug #4234. --- pretyping/evarutil.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6d076ecd11..ee6bbe7fbe 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -795,8 +795,10 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in + let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in + let sort = destSort concl in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s + Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) -- cgit v1.2.3 From 90d52ae25f08c5d1d58685e31073b8f3f37aad49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2015 18:57:06 +0200 Subject: Better error message for non-existent required libraries with a From prefix. --- toplevel/vernacentries.ml | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6272625bda..9d5edc80a0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -379,17 +379,27 @@ let msg_found_library = function msg_info (hov 0 (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file)) -let err_unmapped_library loc qid = +let err_unmapped_library loc ?from qid = let dir = fst (repr_qualid qid) in + let prefix = match from with + | None -> str "." + | Some from -> + str " and prefix " ++ pr_dirpath from ++ str "." + in user_err_loc (loc,"locate_library", - strbrk "Cannot find a physical path bound to logical path " ++ - pr_dirpath dir ++ str".") + strbrk "Cannot find a physical path bound to logical path matching suffix " ++ + pr_dirpath dir ++ prefix) -let err_notfound_library loc qid = +let err_notfound_library loc ?from qid = + let prefix = match from with + | None -> str "." + | Some from -> + str " with prefix " ++ pr_dirpath from ++ str "." + in user_err_loc (loc,"locate_library", - strbrk "Unable to locate library " ++ pr_qualid qid ++ str".") + strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = let (loc,qid) = qualid_of_reference r in @@ -759,8 +769,8 @@ let vernac_require from import qidl = let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in (dir, f) with - | Library.LibUnmappedDir -> err_unmapped_library loc qid - | Library.LibNotFound -> err_notfound_library loc qid + | Library.LibUnmappedDir -> err_unmapped_library loc ?from:root qid + | Library.LibNotFound -> err_notfound_library loc ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then -- cgit v1.2.3 From 3a7095f9f6a09a4461c2124b0020dfe37962de26 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2015 17:47:24 +0200 Subject: Safer typing primitives. Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. --- CHANGES | 15 ++++++++ plugins/cc/ccalgo.ml | 4 +-- plugins/cc/cctac.ml | 16 ++++----- plugins/decl_mode/decl_proof_instr.ml | 10 +++--- plugins/firstorder/instances.ml | 4 +-- plugins/firstorder/sequent.ml | 4 +-- plugins/funind/functional_principles_proofs.ml | 24 ++++++------- plugins/funind/functional_principles_types.ml | 12 +++---- plugins/funind/g_indfun.ml4 | 8 ++--- plugins/funind/glob_term_to_relation.ml | 18 +++++----- plugins/funind/indfun.ml | 8 ++--- plugins/funind/invfun.ml | 20 +++++------ plugins/funind/recdef.ml | 12 +++---- plugins/omega/coq_omega.ml | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- pretyping/cases.ml | 6 ++-- pretyping/coercion.ml | 8 ++--- pretyping/pretyping.ml | 2 +- pretyping/tacred.ml | 2 +- pretyping/typing.ml | 13 +++++-- pretyping/typing.mli | 9 +++-- pretyping/unification.ml | 4 +-- proofs/clenv.ml | 2 +- proofs/logic.ml | 4 +-- proofs/tacmach.ml | 4 +++ proofs/tacmach.mli | 6 ++-- tactics/autorewrite.ml | 4 +-- tactics/class_tactics.ml | 6 ++-- tactics/contradiction.ml | 2 +- tactics/eauto.ml4 | 2 +- tactics/elim.ml | 4 +-- tactics/eqdecide.ml | 4 +-- tactics/equality.ml | 22 ++++++------ tactics/extratactics.ml4 | 4 +-- tactics/hints.ml | 2 +- tactics/hipattern.ml4 | 2 +- tactics/inv.ml | 6 ++-- tactics/rewrite.ml | 16 ++++----- tactics/tacinterp.ml | 2 +- tactics/tacticals.ml | 4 +-- tactics/tactics.ml | 50 +++++++++++++------------- toplevel/auto_ind_decl.ml | 4 +-- toplevel/class.ml | 2 +- toplevel/command.ml | 4 +-- 44 files changed, 196 insertions(+), 163 deletions(-) diff --git a/CHANGES b/CHANGES index cb77c297dd..080b460a86 100644 --- a/CHANGES +++ b/CHANGES @@ -20,6 +20,21 @@ Tactics * "Strict" changes the behavior of an unloaded hint to the one of the fail tactic, allowing to emulate the hopefully future import-scoped hint mechanism. +API + +- Some functions from pretyping/typing.ml and their derivatives were potential + source of evarmap leaks, as they dropped their resulting evarmap. The + situation was clarified by renaming them according to a unsafe_* scheme. Their + sound variant is likewise renamed to their old name. The following renamings + were made. + * Typing.type_of -> unsafe_type_of + * Typing.e_type_of -> type_of + * A new e_type_of function that matches the e_ prefix policy + * Tacmach.pf_type_of -> pf_unsafe_type_of + * A new safe pf_type_of function. + All uses of unsafe_* functions should be eventually eliminated. + + Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 29bca8622b..d5d6bdf749 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -513,7 +513,7 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_type_of state.gls trm in + let typ = pf_unsafe_type_of state.gls trm in let typ = canonize_name typ in let new_node= match t with @@ -836,7 +836,7 @@ let complete_one_class state i= let _,etyp,rest= destProd typ in let id = new_state_var etyp state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = pf_type_of state.gls + let _c = pf_unsafe_type_of state.gls (constr_of_term (term state.uf pac.cnode)) in let _args = List.map (fun i -> constr_of_term (term state.uf i)) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 9952cb0807..9c3a0f7299 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -255,13 +255,13 @@ let new_refine c = Proofview.V82.tactic (refine c) let assert_before n c = Proofview.Goal.enter begin fun gl -> - let evm, _ = Tacmach.New.pf_apply e_type_of gl c in + let evm, _ = Tacmach.New.pf_apply type_of gl c in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) end let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of t = Tacmach.New.pf_type_of gl t in + let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check c @@ -331,7 +331,7 @@ let refute_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl in let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in @@ -341,14 +341,14 @@ let refute_tac c t1 t2 p = end let refine_exact_check c gl = - let evm, _ = pf_apply e_type_of gl c in + let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl in let neweq= new_app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in @@ -373,7 +373,7 @@ let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.nf_enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl in let concl = Proofview.Goal.concl gl in (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) @@ -382,7 +382,7 @@ let discriminate_tac (cstr,u as cstru) p = (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) let identity = Universes.constr_of_global (Lazy.force _I) in - (* let trivial=pf_type_of gls identity in *) + (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in let outtype = mkSort outtype in @@ -486,7 +486,7 @@ let congruence_tac depth l = let f_equal = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) let ty = (* Termops.refresh_universes *) (type_of c1) in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 36273faae2..714cd86341 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -773,7 +773,7 @@ let rec take_tac wits gls = match wits with [] -> tclIDTAC gls | wit::rest -> - let typ = pf_type_of gls wit in + let typ = pf_unsafe_type_of gls wit in tclTHEN (thus_tac wit typ []) (take_tac rest) gls @@ -854,7 +854,7 @@ let start_tree env ind rp = let build_per_info etype casee gls = let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in let (ind,u) = @@ -869,7 +869,7 @@ let build_per_info etype casee gls = | _ -> mind.mind_nparams,None in let params,real_args = List.chop nparams args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let pred= List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in @@ -1228,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let nparams = mind.mind_nparams in let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in let ind', u = destInd hd in let _ = assert (eq_ind ind' ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let elim_pred = List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 5912f0a0c3..c80a8081a3 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -105,7 +105,7 @@ let mk_open_instance id idc gl m t= let evmap=Refiner.project gl in let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_type_of gl idc in + let typ=pf_unsafe_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in @@ -154,7 +154,7 @@ let left_instance_tac (inst,id) continue seq= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in let evmap, _ = - try Typing.e_type_of (pf_env gl) evmap gt + try Typing.type_of (pf_env gl) evmap gt with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 802af04d06..96c4eb01eb 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl = let l = expand_constructor_hints l in let f gr (seq,gl) = let gl, c = pf_eapply Evd.fresh_global gl gr in - let typ=(pf_type_of gl c) in + let typ=(pf_unsafe_type_of gl c) in (add_formula Hyp gr typ seq gl,gl) in List.fold_right f l (seq,gl) @@ -214,7 +214,7 @@ let extend_with_auto_hints l seq gl= | Res_pf_THEN_trivial_fail (c,_) -> (try let gr = global_of_constr c in - let typ=(pf_type_of gl c) in + let typ=(pf_unsafe_type_of gl c) in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4a832435f8..169a706005 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -328,7 +328,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let all_ids = pf_ids_of_hyps g in let new_ids,_ = list_chop ctxt_size all_ids in let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in - let evm, _ = pf_apply Typing.e_type_of g to_refine in + let evm, _ = pf_apply Typing.type_of g to_refine in tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g ) in @@ -543,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id] + scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -593,7 +593,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) - let new_term_value_eq = pf_type_of g' (mkVar heq_id) in + let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in (* compute the new value of the body *) let new_term_value = match kind_of_term new_term_value_eq with @@ -606,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = in let fun_body = mkLambda(Anonymous, - pf_type_of g' term, + pf_unsafe_type_of g' term, Termops.replace_term term (mkRel 1) dyn_infos.info ) in @@ -638,7 +638,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = fun g -> let prov_hid = pf_get_new_id hid g in let c = mkApp(mkVar hid,args) in - let evm, _ = pf_apply Typing.e_type_of g c in + let evm, _ = pf_apply Typing.type_of g c in tclTHENLIST[ Refiner.tclEVARS evm; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); @@ -699,7 +699,7 @@ let build_proof let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in let g_nb_prod = nb_prod (pf_concl g) in - let type_of_term = pf_type_of g t in + let type_of_term = pf_unsafe_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in @@ -919,7 +919,7 @@ let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in - let hyp_typ = pf_type_of g (mkVar hyp) in + let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> if Id.List.mem hyp hyps @@ -964,7 +964,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = - let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f + let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f in decompose_prod_n_assum (nb_params + nb_args) t,evd @@ -1034,8 +1034,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Global.env ()) !evd (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in - let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in - evd:=evd'; + evd:=evd'; + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in res in let nb_intro_to_do = nb_prod (pf_concl g) in @@ -1414,7 +1414,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in - let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in + let _,hrec_concl = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in let f_app = Array.last (snd (destApp hrec_concl)) in let f = (fst (destApp f_app)) in let rec backtrack : tactic = @@ -1641,7 +1641,7 @@ let prove_principle_for_gen (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1)); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *) +(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); (* observe_tac "finish" *) (fun gl' -> diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a2bbf97ae3..3edc590ccc 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -274,7 +274,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") [] in - let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -327,7 +327,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let s = Universes.new_sort_in_family fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in - let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in + let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in ignore( @@ -478,7 +478,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr in let _ = evd := sigma in let l_schemes = - List.map (Typing.type_of env sigma) schemes + List.map (Typing.unsafe_type_of env sigma) schemes in let i = ref (-1) in let sorts = @@ -608,8 +608,8 @@ let build_scheme fas = (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in - let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in - let _ = evd := evd' in + let _ = evd := evd' in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in (destConst f,sort) ) fas @@ -659,7 +659,7 @@ let build_case_scheme fa = in let sigma, scheme = (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in - let scheme_type = (Typing.type_of env sigma ) scheme in + let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in let sorts = (fun (_,_,x) -> Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 043d4328c4..61f03d6f22 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -321,7 +321,7 @@ let mkEq typ c1 c2 = let poseq_unsafe idunsafe cstr gl = - let typ = Tacmach.pf_type_of gl cstr in + let typ = Tacmach.pf_unsafe_type_of gl cstr in tclTHEN (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)) (tclTHENFIRST @@ -349,7 +349,7 @@ let rec poseq_list_ids_rec lcstr gl = let _ = prstr "c = " in let _ = prconstr c in let _ = prstr "\n" in - let typ = Tacmach.pf_type_of gl c in + let typ = Tacmach.pf_unsafe_type_of gl c in let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in let x = Tactics.fresh_id [] cname gl in let _ = list_constr_largs:=mkVar x :: !list_constr_largs in @@ -478,8 +478,8 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF (CRef (Libnames.Ident (Loc.ghost,id1),None)) in let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty (CRef (Libnames.Ident (Loc.ghost,id2),None)) in - let f1type = Typing.type_of (Global.env()) Evd.empty f1 in - let f2type = Typing.type_of (Global.env()) Evd.empty f2 in + let f1type = Typing.unsafe_type_of (Global.env()) Evd.empty f1 in + let f2type = Typing.unsafe_type_of (Global.env()) Evd.empty f2 in let ar1 = List.length (fst (decompose_prod f1type)) in let ar2 = List.length (fst (decompose_prod f2type)) in let _ = diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9e3f398633..065c12a2d7 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -487,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = The "value" of this branch is then simply [res] *) let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in - let rt_typ = Typing.type_of env Evd.empty rt_as_constr in + let rt_typ = Typing.unsafe_type_of env Evd.empty rt_as_constr in let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -595,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env Evd.empty v in - let v_type = Typing.type_of env Evd.empty v_as_constr in + let v_type = Typing.unsafe_type_of env Evd.empty v_as_constr in let new_env = match n with Anonymous -> env @@ -611,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(_,b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> @@ -643,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = nal in let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> @@ -690,7 +690,7 @@ and build_entry_lc_from_case env funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in - Typing.type_of env Evd.empty case_arg_as_constr + Typing.unsafe_type_of env Evd.empty case_arg_as_constr ) el in (****** The next works only if the match is not dependent ****) @@ -737,7 +737,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.fold_right (fun id acc -> let typ_of_id = - Typing.type_of env_with_pat_ids Evd.empty (mkVar id) + Typing.unsafe_type_of env_with_pat_ids Evd.empty (mkVar id) in let raw_typ_of_id = Detyping.detype false [] @@ -791,7 +791,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in + let typ_of_id = Typing.unsafe_type_of new_env Evd.empty (mkVar id) in let raw_typ_of_id = Detyping.detype false [] new_env Evd.empty typ_of_id in @@ -1105,7 +1105,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin let not_free_in_t id = not (is_free_in id t) in let t',ctx = Pretyping.understand env Evd.empty t in - let type_t' = Typing.type_of env Evd.empty t' in + let type_t' = Typing.unsafe_type_of env Evd.empty t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1255,7 +1255,7 @@ let do_build_inductive let evd,env = Array.fold_right2 (fun id c (evd,env) -> - let evd,t = Typing.e_type_of env evd (mkConstU c) in + let evd,t = Typing.type_of env evd (mkConstU c) in evd, Environ.push_named (id,None,t) (* try *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e211b68837..5dcb0c0439 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -72,11 +72,11 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,NoBindings, Tacmach.pf_type_of g' princ,g') + (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') | _ -> raise (UserError("",str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> - princ,binding,Tacmach.pf_type_of g princ,g + princ,binding,Tacmach.pf_unsafe_type_of g princ,g in let princ_infos = Tactics.compute_elim_sig princ_type in let args_as_induction_constr = @@ -356,8 +356,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (fun i x -> let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in - let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in - let _ = evd := evd' in + let _ = evd := evd' in + let princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd uprinc in Functional_principles_types.generate_functional_principle evd interactive_proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d10924f886..89ceb751a4 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -127,8 +127,8 @@ let generate_type evd g_to_f f graph i = let evd',graph = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd graph))) in - let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in evd:=evd'; + let graph_arity = Typing.e_type_of (Global.env ()) evd graph in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -193,7 +193,7 @@ let find_induction_principle evd f = | None -> raise Not_found | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in - let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in + let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in evd:=evd'; rect_lemma,typ @@ -296,7 +296,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let constructor_args g = List.fold_right (fun hid acc -> - let type_of_hid = pf_type_of g (mkVar hid) in + let type_of_hid = pf_unsafe_type_of g (mkVar hid) in match kind_of_term type_of_hid with | Prod(_,_,t') -> begin @@ -440,7 +440,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes "functional_induction" ( (fun gl -> let term = mkApp (mkVar principle_id,Array.of_list bindings) in - let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true) gl term in + let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl term in Proofview.V82.of_tactic (apply term) gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) @@ -577,7 +577,7 @@ let rec reflexivity_with_destruct_cases g = match sc with None -> tclIDTAC g | Some id -> - match kind_of_term (pf_type_of g (mkVar id)) with + match kind_of_term (pf_unsafe_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g @@ -642,7 +642,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in let graph_principle = nf_zeta schemes.(i) in - let princ_type = pf_type_of g graph_principle in + let princ_type = pf_unsafe_type_of g graph_principle in let princ_infos = Tactics.compute_elim_sig princ_type in (* Then we get the number of argument of the function and compute a fresh name for each of them @@ -772,7 +772,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in + let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info @@ -900,7 +900,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing *) let revert_graph kn post_tac hid g = - let typ = pf_type_of g (mkVar hid) in + let typ = pf_unsafe_type_of g (mkVar hid) in match kind_of_term typ with | App(i,args) when isInd i -> let ((kn',num) as ind'),u = destInd i in @@ -951,7 +951,7 @@ let revert_graph kn post_tac hid g = let functional_inversion kn hid fconst f_correct : tactic = fun g -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in - let type_of_h = pf_type_of g (mkVar hid) in + let type_of_h = pf_unsafe_type_of g (mkVar hid) in match kind_of_term type_of_h with | App(eq,args) when eq_constr eq (make_eq ()) -> let pre_tac,f_args,res = @@ -1003,7 +1003,7 @@ let invfun qhyp f g = Proofview.V82.of_tactic begin Tactics.try_intros_until (fun hid -> Proofview.V82.tactic begin fun g -> - let hyp_typ = pf_type_of g (mkVar hid) in + let hyp_typ = pf_unsafe_type_of g (mkVar hid) in match kind_of_term hyp_typ with | App(eq,args) when eq_constr eq (make_eq ()) -> begin diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b9902a9fc7..d3979748e1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -115,7 +115,7 @@ let pf_get_new_ids idl g = let compute_renamed_type gls c = rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] - (pf_type_of gls c) + (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" @@ -400,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = thin to_intros; h_intros to_intros; (fun g' -> - let ty_teq = pf_type_of g' (mkVar heq) in + let ty_teq = pf_unsafe_type_of g' (mkVar heq) in let teq_lhs,teq_rhs = let _,args = try destApp ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -514,13 +514,13 @@ let rec prove_lt hyple g = in let h = List.find (fun id -> - match decompose_app (pf_type_of g (mkVar id)) with + match decompose_app (pf_unsafe_type_of g (mkVar id)) with | _, t::_ -> eq_constr t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in observe_tclTHENLIST (str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (str "prove_lt") (prove_lt hyple) @@ -655,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} let pf_type c tac gl = - let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in + let evars, ty = Typing.type_of (pf_env gl) (project gl) c in tclTHEN (Refiner.tclEVARS evars) (tac ty) gl let pf_typel l tac = @@ -680,7 +680,7 @@ let mkDestructEq : if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in - let type_of_expr = pf_type_of g expr in + let type_of_expr = pf_unsafe_type_of g expr in let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4e2696dfdb..710a2394d3 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1689,7 +1689,7 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.nf_enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = Tacmach.New.of_old decidability gl in let pf_nf = Tacmach.New.of_old pf_nf gl in let rec loop = function diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 2f9e8509c2..e590958ccf 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -162,7 +162,7 @@ let ic_unsafe c = (*FIXME remove *) let env = Global.env() and sigma = Evd.empty in fst (Constrintern.interp_constr env sigma c) -let ty c = Typing.type_of (Global.env()) Evd.empty c +let ty c = Typing.unsafe_type_of (Global.env()) Evd.empty c let decl_constant na ctx c = let vars = Universes.universes_of_constr c in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fcbe90b6a7..ef196e0a72 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1668,7 +1668,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.e_type_of extenv !evdref t in + let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in @@ -2014,7 +2014,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env - {uj_val = ty; uj_type = Typing.type_of env !evdref ty} + {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} in let (ind,u), params = dest_ind_family indf in if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind; @@ -2214,7 +2214,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in + let _btype = evd_comb1 (Typing.type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 8ebb8cd27b..f5135f5c60 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let evm = !evdref in (try subco () with NoSubtacCoercion -> - let typ = Typing.type_of env evm c in - let typ' = Typing.type_of env evm c' in + let typ = Typing.unsafe_type_of env evm c in + let typ' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm typ) then *) coerce_application typ typ' c c' l l') (* else subco () *) @@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) | x, y when Constr.equal c c' -> if Int.equal (Array.length l) (Array.length l') then let evm = !evdref in - let lam_type = Typing.type_of env evm c in - let lam_type' = Typing.type_of env evm c' in + let lam_type = Typing.unsafe_type_of env evm c in + let lam_type' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm lam_type) then ( *) coerce_application lam_type lam_type' c c' l l' (* ) else subco () *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0cadffa4fe..03fe2122c0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -374,7 +374,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.type_of env evd c in + let ty = Typing.unsafe_type_of env evd c in make_judge c ty let judge_of_Type evd s = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 372b26aa25..8a5db90590 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1134,7 +1134,7 @@ let abstract_scheme env (locc,a) (c, sigma) = let pattern_occs loccs_trm env sigma c = let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in try - let _ = Typing.type_of env sigma abstr_trm in + let _ = Typing.unsafe_type_of env sigma abstr_trm in sigma, applist(abstr_trm, List.map snd loccs_trm) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c6209cc33a..fb5927dbf7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -270,7 +270,7 @@ let check env evdref c t = (* Type of a constr *) -let type_of env evd c = +let unsafe_type_of env evd c = let j = execute env (ref evd) c in j.uj_type @@ -283,7 +283,7 @@ let sort_of env evdref c = (* Try to solve the existential variables by typing *) -let e_type_of ?(refresh=false) env evd c = +let type_of ?(refresh=false) env evd c = let evdref = ref evd in let j = execute env evdref c in (* side-effect on evdref *) @@ -291,6 +291,15 @@ let e_type_of ?(refresh=false) env evd c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type else !evdref, j.uj_type +let e_type_of ?(refresh=false) env evdref c = + let j = execute env evdref c in + (* side-effect on evdref *) + if refresh then + let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in + let () = evdref := evd in + c + else j.uj_type + let solve_evars env evdref c = let c = (execute env evdref c).uj_val in (* side-effect on evdref *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1f822f1a58..bfae46ff80 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -13,12 +13,15 @@ open Evd (** This module provides the typing machine with existential variables and universes. *) -(** Typecheck a term and return its type *) -val type_of : env -> evar_map -> constr -> types +(** Typecheck a term and return its type. May trigger an evarmap leak. *) +val unsafe_type_of : env -> evar_map -> constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types +val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types + +(** Variant of [type_of] using references instead of state-passing. *) +val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) val sort_of : env -> evar_map ref -> types -> sorts diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c2281e13a5..b5fe5d0b6d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -93,7 +93,7 @@ let abstract_list_all env evd typ c l = let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in let evd,typp = - try Typing.e_type_of env evd p + try Typing.type_of env evd p with | UserError _ -> error_cannot_find_well_typed_abstraction env evd p l None @@ -1150,7 +1150,7 @@ let applyHead env evd n c = apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.type_of env evd c) evd + apprec n c (Typing.unsafe_type_of env evd c) evd let is_mimick_head ts f = match kind_of_term f with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2c9c695bfd..a2cccc0e0b 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -28,7 +28,7 @@ open Misctypes (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c +let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c (******************************************************************) (* Clausal environments *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 898588d9e4..5c48995fc7 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -83,7 +83,7 @@ let apply_to_hyp sign id f = else sign let check_typability env sigma c = - if !check then let _ = type_of env sigma c in () + if !check then let _ = unsafe_type_of env sigma c in () (************************************************************************) (************************************************************************) @@ -317,7 +317,7 @@ let meta_free_prefix a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then type_of env sigma c + if !check then unsafe_type_of env sigma c else Retyping.get_type_of env sigma c let rec mk_refgoals sigma goal goalacc conclty trm = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index fa0d03623c..4238d1e372 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -84,6 +84,7 @@ let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of @@ -172,6 +173,9 @@ module New = struct let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl + let pf_unsafe_type_of gl t = + pf_apply unsafe_type_of gl t + let pf_type_of gl t = pf_apply type_of gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f7fc6b54f1..a0e1a01577 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,7 +41,8 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_type_of : goal sigma -> constr -> types +val pf_unsafe_type_of : goal sigma -> constr -> types +val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types val pf_get_hyp : goal sigma -> Id.t -> named_declaration @@ -112,7 +113,8 @@ module New : sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_concl : [ `NF ] Proofview.Goal.t -> types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ad8164fa64..2b3fadf7fa 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -263,7 +263,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 + Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) @@ -281,7 +281,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation metas loc env sigma c left2right = - let ctype = Typing.type_of env sigma c in + let ctype = Typing.unsafe_type_of env sigma c in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6ea25269cf..ef78a953ac 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -149,7 +149,7 @@ let e_give_exact flags poly (c,clenv) gl = c, {gl with sigma = clenv'.evd} else c, gl in - let t1 = pf_type_of gl c in + let t1 = pf_unsafe_type_of gl c in tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = @@ -168,7 +168,7 @@ let unify_resolve poly flags (c,clenv) gls = let clenv_of_prods poly nprods (c, clenv) gls = if poly || Int.equal nprods 0 then Some clenv else - let ty = pf_type_of gls c in + let ty = pf_unsafe_type_of gls c in let diff = nb_prod ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) @@ -842,6 +842,6 @@ let is_ground c gl = let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_type_of gl c in + let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in unify_e_resolve false flags (c,ce) gl diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c03710e911..22f218b4fb 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -90,7 +90,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.nf_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 50925ecde6..34f87c6cf0 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -33,7 +33,7 @@ DECLARE PLUGIN "eauto" let eauto_unif_flags = auto_flags_of_state full_transparent_state -let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in +let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_unsafe_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 || occur_existential t2 then tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl else Proofview.V82.of_tactic (exact_check c) gl diff --git a/tactics/elim.ml b/tactics/elim.ml index 3cb4fa9c4c..4841d2c252 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -85,7 +85,7 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> - let type_of = pf_type_of gl in + let type_of = pf_unsafe_type_of gl in let typc = type_of c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) @@ -139,7 +139,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.nf_enter begin fun gl -> - let idty = pf_type_of gl (mkVar id) in + let idty = pf_unsafe_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) idty in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 2ee4bf8e12..a5d68e19bd 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -133,7 +133,7 @@ let match_eqdec c = let solveArg eqonleft op a1 a2 tac = Proofview.Goal.enter begin fun gl -> - let rectype = pf_type_of gl a1 in + let rectype = pf_unsafe_type_of gl a1 in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let subtacs = if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto] @@ -203,7 +203,7 @@ let decideEquality rectype = let compare c1 c2 = Proofview.Goal.enter begin fun gl -> - let rectype = pf_type_of gl c1 in + let rectype = pf_unsafe_type_of gl c1 in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro diff --git a/tactics/equality.ml b/tactics/equality.ml index 593b7e9ea0..fb7237e4b2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -165,7 +165,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = - let ct = pf_type_of gl c in + let ct = pf_unsafe_type_of gl c in let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in [eqclause] @@ -944,7 +944,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.nf_enter begin fun gl -> - let type_of = pf_type_of gl in + let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in let t = type_of c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in @@ -1019,7 +1019,7 @@ let find_sigma_data env s = build_sigma_type () let make_tuple env sigma (rterm,rty) lind = assert (dependent (mkRel lind) rty); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in - let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in + let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in let (na,_,_) = lookup_rel lind env in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in @@ -1053,7 +1053,7 @@ let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in let combined_rels = Int.Set.union prev_rels direct_rels in - let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i))) in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) in minimalrec_free_rels_rec Int.Set.empty @@ -1099,7 +1099,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let rec sigrec_clausal_form siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) - let dflt_typ = type_of env sigma dflt in + let dflt_typ = unsafe_type_of env sigma dflt in try let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in @@ -1118,7 +1118,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (destEvar ev) with | Some w -> - let w_type = type_of env sigma w in + let w_type = unsafe_type_of env sigma w in if Evarconv.e_cumul env evdref w_type a then let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) @@ -1200,7 +1200,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1253,7 +1253,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in @@ -1293,7 +1293,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let injfun = mkNamedLambda e t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in let pf = applist(congr,[t;resty;injfun;t1;t2]) in - let sigma, pf_typ = Typing.e_type_of env sigma pf in + let sigma, pf_typ = Typing.type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in let pf = Clenvtac.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in @@ -1460,8 +1460,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) let expected_goal = nf_betaiota sigma expected_goal in (* Retype to get universes right *) - let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in - let sigma, _ = Typing.e_type_of env sigma body in + let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in + let sigma, _ = Typing.type_of env sigma body in sigma,body,expected_goal (* Like "replace" but decompose dependent equalities *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f217cda894..177be2c205 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -704,7 +704,7 @@ let refl_equal = call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); Proofview.Goal.nf_enter begin fun gl -> @@ -755,7 +755,7 @@ let destauto t = let destauto_in id = Proofview.Goal.nf_enter begin fun gl -> - let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype diff --git a/tactics/hints.ml b/tactics/hints.ml index ae45aabd0b..0df1a35c62 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -780,7 +780,7 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (type_of env sigma c) in + let t = hnf_constr env sigma (unsafe_type_of env sigma c) in let hd = head_of_constr_reference (head_constr t) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 4b94f420ba..95f3af57e2 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -411,7 +411,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *) let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_type_of gl e1 in (t,e1,e2) + let t = pf_unsafe_type_of gl e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if pf_conv_x gl t1 t2 then (t1,e1,e2) diff --git a/tactics/inv.ml b/tactics/inv.ml index 5502356fbf..ef115aea0e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl = let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args @@ -437,7 +437,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in Errors.errorlabstrm "" msg diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index d487317736..6d26e91c68 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -381,7 +381,7 @@ end let type_app_poly env env evd f args = let evars, c = app_poly_nocheck env evd f args in - let evd', t = Typing.e_type_of env (goalevars evars) c in + let evd', t = Typing.type_of env (goalevars evars) c in (evd', cstrevars evars), c module PropGlobal = struct @@ -472,7 +472,7 @@ let rec decompose_app_rel env evd t = | App (f, [||]) -> assert false | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in - let ty = Typing.type_of env evd argl in + let ty = Typing.unsafe_type_of env evd argl in let f'' = mkLambda (Name default_dependent_ident, ty, mkLambda (Name (Id.of_string "y"), lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) @@ -747,7 +747,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in - let appmtype = Typing.type_of env (goalevars evars) appm in + let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1738,7 +1738,7 @@ let declare_projection n instance_id r = let poly = Global.is_polymorphic r in let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in let term = proper_projection c ty in - let typ = Typing.type_of (Global.env ()) Evd.empty term in + let typ = Typing.unsafe_type_of (Global.env ()) Evd.empty term in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1771,7 +1771,7 @@ let build_morphism_signature m = let env = Global.env () in let m,ctx = Constrintern.interp_constr env Evd.empty m in let sigma = Evd.from_env ~ctx env in - let t = Typing.type_of env sigma m in + let t = Typing.unsafe_type_of env sigma m in let cstrs = let rec aux t = match kind_of_term t with @@ -1798,7 +1798,7 @@ let build_morphism_signature m = let default_morphism sign m = let env = Global.env () in - let t = Typing.type_of env Evd.empty m in + let t = Typing.unsafe_type_of env Evd.empty m in let evars, _, sign, cstrs = PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -1994,7 +1994,7 @@ let setoid_proof ty fn fallback = try let rel, _, _ = decompose_app_rel env sigma concl in let evm = sigma in - let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in + let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in (try init_setoid () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e @@ -2053,7 +2053,7 @@ let setoid_transitivity c = let setoid_symmetry_in id = Proofview.V82.tactic (fun gl -> - let ctype = pf_type_of gl (mkVar id) in + let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum ctype in let (equiv, args) = decompose_app concl in let rec split_last_two = function diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7ce158fd1a..374c7c7364 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -734,7 +734,7 @@ let interp_may_eval f ist env sigma = function str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - Typing.e_type_of ~refresh:true env sigma c_interp + Typing.type_of ~refresh:true env sigma c_interp | ConstrTerm c -> try f ist env sigma c diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5ba53a7641..7d1cc3341c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -598,7 +598,7 @@ module New = struct (** FIXME: evar leak. *) let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in (* applying elimination_scheme just a little modified *) - let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -651,7 +651,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.nf_enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3038a95068..2791d7c484 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -158,7 +158,7 @@ let convert_concl ?(check=true) ty k = Proofview.Refine.refine ~unsafe:true begin fun sigma -> let sigma = if check then begin - ignore (Typing.type_of env sigma ty); + ignore (Typing.unsafe_type_of env sigma ty); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; sigma @@ -628,7 +628,7 @@ let change_on_subterm cv_pb deep t where env sigma c = env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.type_of env sigma c) + try ignore (Typing.unsafe_type_of env sigma c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." end; @@ -979,7 +979,7 @@ let cut c = let is_sort = try (** Backward compat: ensure that [c] is well-typed. *) - let typ = Typing.type_of env sigma c in + let typ = Typing.unsafe_type_of env sigma c in let typ = whd_betadeltaiota env sigma typ in match kind_of_term typ with | Sort _ -> true @@ -1224,7 +1224,7 @@ let find_ind_eliminator ind s gl = evd, c let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in + let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); @@ -1639,7 +1639,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let cut_and_apply c = Proofview.Goal.nf_enter begin fun gl -> - match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with + match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in @@ -1672,7 +1672,7 @@ let exact_check c = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, ct = Typing.e_type_of env sigma c in + let sigma, ct = Typing.type_of env sigma c in Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) end @@ -1821,7 +1821,7 @@ let specialize (c,lbind) g = let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in tclEVARS evd, nf_evar evd c else - let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in + let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in @@ -1841,11 +1841,11 @@ let specialize (c,lbind) g = | Var id when Id.List.mem id (pf_ids_of_hyps g) -> tclTHEN tac (tclTHENFIRST - (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g) (exact_no_check term)) g | _ -> tclTHEN tac (tclTHENLAST - (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g) (exact_no_check term)) g (* Keeping only a few hypotheses *) @@ -1980,7 +1980,7 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq loc l thin tac id = Proofview.Goal.nf_enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> @@ -1994,7 +1994,7 @@ let intro_decomp_eq loc l thin tac id = let intro_or_and_pattern loc bracketed ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in let nv = constructors_nrealargs ind in let ll = fix_empty_or_and_pattern (Array.length nv) ll in @@ -2013,7 +2013,7 @@ let rewrite_hyp assert_style l2r id = let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in let t = whd_betadeltaiota (type_of (mkVar id)) in match match_with_equality_type t with @@ -2290,7 +2290,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in - let sigma, _ = Typing.e_type_of env sigma term in + let sigma, _ = Typing.type_of env sigma term in sigma, term, Tacticals.New.tclTHEN (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) @@ -2376,7 +2376,7 @@ let forward b usetac ipat c = match usetac with | None -> Proofview.Goal.enter begin fun gl -> - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c)) end @@ -2459,7 +2459,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) = mkProd_or_LetIn (na,b,t) cl', evd' let generalize_goal gl i ((occs,c,b),na as o) cl = - let t = pf_type_of gl c in + let t = pf_unsafe_type_of gl c in let env = pf_env gl in generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl @@ -2520,7 +2520,7 @@ let new_generalize_gen_let lconstr = let (newcl, sigma), args = List.fold_right_i (fun i ((_,c,b),_ as o) (cl, args) -> - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let args = if Option.is_empty b then c :: args else args in generalize_goal_gen env ids i o t cl, args) 0 lconstr ((concl, sigma), []) @@ -2797,7 +2797,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match kind_of_term c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN @@ -3201,7 +3201,7 @@ let abstract_args gl generalize_vars dep id defined f args = let rel, c = Reductionops.splay_prod_n env sigma 1 prod in List.hd rel, c in - let argty = pf_type_of gl arg in + let argty = pf_unsafe_type_of gl arg in let ty = (* refresh_universes_strict *) ty in let lenctx = List.length ctx in let liftargty = lift lenctx argty in @@ -3242,7 +3242,7 @@ let abstract_args gl generalize_vars dep id defined f args = in if dogen then let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + Array.fold_left aux (pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -3566,13 +3566,13 @@ let guess_elim isrec dep s hyp0 gl = Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s else Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in - let elimt = Tacmach.New.pf_type_of gl elimc in + let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in evd, ((elimc, NoBindings), elimt), mkIndU mind let given_elim hyp0 (elimc,lbind as e) gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in - Proofview.Goal.sigma gl, (e, Tacmach.New.pf_type_of gl elimc), ind_type_guess + Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = (Id.t list * (elim_arg_kind * bool * Id.t) list) array @@ -3604,7 +3604,7 @@ let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = - let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in + let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -3963,7 +3963,7 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -4225,7 +4225,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_type_of gl (mkVar id) in + let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE begin @@ -4276,7 +4276,7 @@ let prove_transitivity hdcncl eq_kind t = | HeterogenousEq (typ1,c1,typ2,c2) -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let type_of = Typing.type_of env sigma in + let type_of = Typing.unsafe_type_of env sigma in let typt = type_of t in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 96bb89e2a4..f905080905 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -355,7 +355,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = ) in Proofview.Goal.nf_enter begin fun gl -> - let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in + let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = try @@ -417,7 +417,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter begin fun gl -> - let tt1 = Tacmach.New.pf_type_of gl t1 in + let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in if eq_constr t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind tt1 diff --git a/toplevel/class.ml b/toplevel/class.ml index 6a485d52c0..0e270f960b 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly = let _ = if not (Reductionops.is_conv_leq env Evd.empty - (Typing.type_of env Evd.empty val_f) typ_f) + (Typing.unsafe_type_of env Evd.empty val_f) typ_f) then errorlabstrm "" (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") diff --git a/toplevel/command.ml b/toplevel/command.ml index 1249581eec..7cf0477f9f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -847,7 +847,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in - let relty = Typing.type_of env !evdref rel in + let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = user_err_loc (constr_loc r, @@ -988,7 +988,7 @@ let interp_recursive isfix fixl notations = List.fold_left2 (fun env' id t -> if Flags.is_program_mode () then - let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in + let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in -- cgit v1.2.3 From d91addb140ba7315d70c4599b0d058bef798ac1c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2015 23:38:55 +0200 Subject: Fixing bug #4216: Internal error: Anomaly: Uncaught exception Not_found. Please report. An evarmap was lost because of an unsound typing primitive. --- tactics/equality.ml | 8 ++++---- test-suite/bugs/closed/4216.v | 20 ++++++++++++++++++++ 2 files changed, 24 insertions(+), 4 deletions(-) create mode 100644 test-suite/bugs/closed/4216.v diff --git a/tactics/equality.ml b/tactics/equality.ml index fb7237e4b2..ea74dc37ea 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -165,10 +165,10 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = - let ct = pf_unsafe_type_of gl c in - let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in - let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in - [eqclause] + let sigma, ct = pf_type_of gl c in + let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in + let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in + [eqclause] let rewrite_conv_closed_core_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v new file mode 100644 index 0000000000..ae7f746778 --- /dev/null +++ b/test-suite/bugs/closed/4216.v @@ -0,0 +1,20 @@ +Generalizable Variables T A. + +Inductive path `(a: A): A -> Type := idpath: path a a. + +Class TMonad (T: Type -> Type) := { + bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B; + ret: forall {A: Type}, A -> T A; + ret_unit_left: forall {A B: Type} (k: A -> T B) (a: A), + path (bind (ret a) k) (k a) + }. + +Let T_fzip `{TMonad T} := fun (A B: Type) (f: T (A -> B)) (t: T A) + => bind t (fun a => bind f (fun g => ret (g a) )). +Let T_pure `{TMonad T} := @ret _ _. + +Let T_pure_id `{TMonad T} {A: Type} (t: A -> A) (x: T A): + path (T_fzip A A (T_pure (A -> A) t) x) x. + unfold T_fzip, T_pure. + Fail rewrite (ret_unit_left (fun g a => ret (g a)) (fun x => x)). + -- cgit v1.2.3 From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 14 May 2015 09:53:36 +0200 Subject: Disable precompilation for native_compute by default. Note that this does not prevent using native_compute, but it will force on-the-fly recompilation of dependencies whenever it is used. Precompilation is enabled for the standard library, assuming native compilation was enabled at configuration time. If native compilation was disabled at configuration time, native_compute falls back to vm_compute. Failure to precompile is a hard error, since it is now explicitly required by the user. --- Makefile.build | 2 +- configure.ml | 4 +++- kernel/nativeconv.ml | 5 ++--- kernel/safe_typing.ml | 4 ++-- lib/flags.ml | 4 ++-- lib/flags.mli | 4 ++-- library/library.ml | 6 +++--- pretyping/nativenorm.ml | 4 ++-- proofs/redexpr.ml | 10 +++++++--- tools/coqc.ml | 2 +- toplevel/coqtop.ml | 5 ++++- toplevel/usage.ml | 2 +- 12 files changed, 30 insertions(+), 22 deletions(-) diff --git a/Makefile.build b/Makefile.build index 018471b684..41220792d5 100644 --- a/Makefile.build +++ b/Makefile.build @@ -81,7 +81,7 @@ TIMECMD= # if you prefer a specific time command instead of $(STDTIME) STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) -COQOPTS=$(COQ_XML) $(VM) +COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands diff --git a/configure.ml b/configure.ml index 68fe7e1211..1916e82172 100644 --- a/configure.ml +++ b/configure.ml @@ -1199,7 +1199,9 @@ let write_makefile f = pr "# Defining REVISION\n"; pr "CHECKEDOUT=%s\n\n" vcs; pr "# Option to control compilation and installation of the documentation\n"; - pr "WITHDOC=%s\n" (if withdoc then "all" else "no"); + pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no"); + pr "# Option to produce precompiled files for native_compute\n"; + pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else ""); close_out o; Unix.chmod f 0o444 diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 75a3fc4582..1f8bfc984f 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -121,9 +121,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu = aux 0 let native_conv pb sigma env t1 t2 = - if !Flags.no_native_compiler then begin - let msg = "Native compiler is disabled, "^ - "falling back to VM conversion test." in + if Coq_config.no_native_compiler then begin + let msg = "Native compiler is disabled, falling back to VM conversion test." in Pp.msg_warning (Pp.str msg); vm_conv pb env t1 t2 end diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d762a246e6..d6bd754783 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -772,9 +772,9 @@ let export ?except senv dir = } in let ast, values = - if !Flags.no_native_compiler then [], [||] - else + if !Flags.native_compiler then Nativelibrary.dump_library mp dir senv.env str + else [], [||] in let lib = { comp_name = dir; diff --git a/lib/flags.ml b/lib/flags.ml index c8e7f7afed..f87dd5c2c8 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -206,8 +206,8 @@ let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level -(* Disabling native code compilation for conversion and normalization *) -let no_native_compiler = ref Coq_config.no_native_compiler +(* Native code compilation for conversion and normalization *) +let native_compiler = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 756d3b8515..1f68a88f3a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -128,8 +128,8 @@ val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(* Disabling native code compilation for conversion and normalization *) -val no_native_compiler : bool ref +(* Native code compilation for conversion and normalization *) +val native_compiler : bool ref (* Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref diff --git a/library/library.ml b/library/library.ml index 1ffa1a305c..0296d7b906 100644 --- a/library/library.ml +++ b/library/library.ml @@ -166,7 +166,7 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - if not !Flags.no_native_compiler then + if !Flags.native_compiler then Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function @@ -788,10 +788,10 @@ let save_library_to ?todo dir f otab = System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) - if not !Flags.no_native_compiler then + if !Flags.native_compiler then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then - msg_error (str"Could not compile the library to native code. Skipping.") + error "Could not compile the library to native code." with reraise -> let reraise = Errors.push reraise in let () = msg_warning (str "Removed file " ++ str f') in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index bd427ecd08..ac4e3b3064 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -378,8 +378,8 @@ and nf_predicate env ind mip params v pT = | _, _ -> false, nf_type env v let native_norm env sigma c ty = - if !Flags.no_native_compiler then - error "Native_compute reduction has been disabled" + if Coq_config.no_native_compiler then + error "Native_compute reduction has been disabled at configure time." else let penv = Environ.pre_env env in (* diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d25f7e9150..f172bbdd1a 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -30,9 +30,13 @@ let cbv_vm env sigma c = Vnorm.cbv_vm env c ctyp let cbv_native env sigma c = - let ctyp = Retyping.get_type_of env sigma c in - let evars = Nativenorm.evars_of_evar_map sigma in - Nativenorm.native_norm env evars c ctyp + if Coq_config.no_native_compiler then + let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in + cbv_vm env sigma c + else + let ctyp = Retyping.get_type_of env sigma c in + let evars = Nativenorm.evars_of_evar_map sigma in + Nativenorm.native_norm env evars c ctyp let whd_cbn flags env sigma t = let (state,_) = diff --git a/tools/coqc.ml b/tools/coqc.ml index 7e822dbe36..31e0a0e0ad 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -109,7 +109,7 @@ let parse_args () = |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" - |"-impredicative-set"|"-vm"|"-no-native-compiler" + |"-impredicative-set"|"-vm"|"-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" |"-indices-matter"|"-quick"|"-color"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2df7c69c86..0a14a19507 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -498,7 +498,10 @@ let parse_args arglist = |"-noinit"|"-nois" -> load_init := false |"-no-compat-notations" -> no_compat_ntn := true |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true - |"-no-native-compiler" -> no_native_compiler := true + |"-native-compiler" -> + if Coq_config.no_native_compiler then + warning "Native compilation was disabled at configure time." + else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true |"-q" -> no_load_rc () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f053839c70..94c1699c2a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -71,7 +71,7 @@ let print_usage_channel co command = \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ \n -time display the time taken by each command\ -\n -no-native-compiler disable the native_compute reduction machinery\ +\n -native-compiler precompile files for the native_compute machinery\ \n -h, -help print this list of options\ \n"; List.iter (fun (name, text) -> -- cgit v1.2.3 From 81eb133d64ac81cbf6962d624b20c1aa55c2baae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 Apr 2015 11:16:05 +0200 Subject: Adding an option -w to control Coq warning output. For now, warnings are still ignored by default, but this may change. This commit at least allows to print them whenever desired. The -w syntax is also opened to future additions to further control the display of warnings. --- CHANGES | 4 ++++ lib/flags.ml | 2 +- tools/coqc.ml | 2 +- toplevel/coqtop.ml | 8 +++++++- toplevel/usage.ml | 5 ++++- toplevel/vernac.ml | 1 - 6 files changed, 17 insertions(+), 5 deletions(-) diff --git a/CHANGES b/CHANGES index 080b460a86..d2890f7402 100644 --- a/CHANGES +++ b/CHANGES @@ -35,6 +35,10 @@ API All uses of unsafe_* functions should be eventually eliminated. +Tools + +- Added an option -w to control the output of coqtop warnings. + Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/lib/flags.ml b/lib/flags.ml index f87dd5c2c8..313da0c5bd 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -160,7 +160,7 @@ let make_polymorphic_flag b = let program_mode = ref false let is_program_mode () = !program_mode -let warn = ref true +let warn = ref false let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x diff --git a/tools/coqc.ml b/tools/coqc.ml index 31e0a0e0ad..aed229abc8 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -122,7 +122,7 @@ let parse_args () = |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" - |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w" as o) :: rem -> begin match rem with diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0a14a19507..160e549afe 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -114,6 +114,11 @@ let set_hierarchy () = if !type_in_type then Global.set_type_in_type () let set_batch_mode () = batch_mode := true +let set_warning = function +| "all" -> make_warn true +| "none" -> make_warn false +| _ -> prerr_endline ("Error: all/none expected after option w"); exit 1 + let toplevel_default_name = DirPath.make [Id.of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) let set_toplevel_name dir = @@ -472,6 +477,7 @@ let parse_args arglist = |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo |"-toploop" -> toploop := Some (next ()) + |"-w" -> set_warning (next ()) (* Options with zero arg *) |"-async-queries-always-delegate" @@ -505,7 +511,7 @@ let parse_args arglist = |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true |"-q" -> no_load_rc () - |"-quiet"|"-silent" -> Flags.make_silent true + |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 94c1699c2a..50fb019f47 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -56,6 +56,10 @@ let print_usage_channel co command = \n -v print Coq version and exit\ \n -list-tags print highlight color tags known by Coq and exit\ \n\ +\n -quiet unset display of extra information (implies -w none)\ +\n -w (all|none) configure display of warnings\ +\n -color (on|off|auto) configure color output (only active through coqtop)\ +\n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ \n -batch batch mode (exits just after arguments parsing)\ @@ -63,7 +67,6 @@ let print_usage_channel co command = \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ \n -emacs tells Coq it is executed under Emacs\ -\n -color (on|off|auto) configure color output (only active through coqtop)\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 96daf5075d..5418c60e94 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -257,7 +257,6 @@ let rec vernac_com verbosely checknav (loc,com) = else iraise (reraise, info) and read_vernac_file verbosely s = - Flags.make_warn verbosely; let checknav loc cmd = if is_navigation_vernac cmd && not (is_reset cmd) then user_error loc "Navigation commands forbidden in files" -- cgit v1.2.3 From 5f8dc36fb2d65699233b9ac9a3ff9f93701a01cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 May 2015 12:49:41 +0200 Subject: The -list-tag options now prints the corresponding COQ_COLORS value. --- lib/terminal.ml | 7 +++++-- lib/terminal.mli | 3 +++ toplevel/coqtop.ml | 11 ++++++++++- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/lib/terminal.ml b/lib/terminal.ml index 0f6b23af36..58851ed274 100644 --- a/lib/terminal.ml +++ b/lib/terminal.ml @@ -117,7 +117,7 @@ let is_extended = function | `INDEX _ | `RGB _ -> true | _ -> false -let eval st = +let repr st = let fg = match st.fg_color with | None -> [] | Some c -> @@ -152,7 +152,10 @@ let eval st = | Some true -> [7] | Some false -> [27] in - let tags = fg @ bg @ bold @ italic @ underline @ negative in + fg @ bg @ bold @ italic @ underline @ negative + +let eval st = + let tags = repr st in let tags = List.map string_of_int tags in Printf.sprintf "\027[%sm" (String.concat ";" tags) diff --git a/lib/terminal.mli b/lib/terminal.mli index f308ede323..49172e3ce3 100644 --- a/lib/terminal.mli +++ b/lib/terminal.mli @@ -46,6 +46,9 @@ val make : ?fg_color:color -> ?bg_color:color -> val merge : style -> style -> style (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *) +val repr : style -> int list +(** Generate the ANSI code representing the given style. *) + val eval : style -> string (** Generate an escape sequence from a style. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 160e549afe..af7169ad6c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -281,7 +281,16 @@ let print_style_tags () = in print_string opt in - List.iter iter tags; + let make (t, st) = match st with + | None -> None + | Some st -> + let tags = List.map string_of_int (Terminal.repr st) in + let t = String.concat "." (Ppstyle.repr t) in + Some (t ^ "=" ^ String.concat ";" tags) + in + let repr = List.map_filter make tags in + let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in + let () = List.iter iter tags in flush_all () let error_missing_arg s = -- cgit v1.2.3 From 3fb81febe8efc34860688cac88a2267cfe298cf7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 14 May 2015 16:38:21 +0200 Subject: Do not regenerate .d files when cleaning them. (Fix bug #4079) --- tools/coq_makefile.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 00088570b3..8f4772e286 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -575,8 +575,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other let decl_var var = function |[] -> () |l -> - printf "%s:=" var; print_list "\\\n " l; print "\n"; - printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var + printf "%s:=" var; print_list "\\\n " l; print "\n\n"; + print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "else\nifeq ($(MAKECMDGOALS),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "endif\nendif\n\n"; + printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var in section "Files dispatching."; decl_var "VFILES" vfiles; -- cgit v1.2.3