diff options
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index b90a911a..98885af8 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -121,7 +121,7 @@ let is_applied_rewrite_relation env sigma rels t = let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in let _ = Typeclasses.resolve_one_typeclass env' evd inst in Some (it_mkProd_or_LetIn t rels) - with _ -> None) + with e when Errors.noncritical e -> None) | _ -> None let _ = @@ -145,11 +145,14 @@ let build_signature evars env m (cstrs : (types * types option) option list) new_cstr_evar evars env (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in - let mk_relty evars env ty obj = + let mk_relty evars newenv ty obj = match obj with | None | Some (_, None) -> let relty = mk_relation ty in - new_evar evars env relty + if closed0 ty then + let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in + new_evar evars env' relty + else new_evar evars newenv relty | Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = @@ -227,7 +230,7 @@ let cstrevars evars = snd evars let evd_convertible env evd x y = try ignore(Evarconv.the_conv_x env x y evd); true - with _ -> false + with e when Errors.noncritical e -> false let rec decompose_app_rel env evd t = match kind_of_term t with @@ -493,7 +496,7 @@ let rec apply_pointwise rel = function | [] -> rel let pointwise_or_dep_relation n t car rel = - if noccurn 1 car then + if noccurn 1 car && noccurn 1 rel then mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |]) else mkApp (Lazy.force forall_relation, @@ -1048,7 +1051,8 @@ module Strategies = let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1056,7 +1060,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None let fold_glob c : strategy = fun env avoid t ty cstr evars -> @@ -1064,7 +1068,8 @@ module Strategies = let sigma, c = Pretyping.Default.understand_tcc (goalevars evars) env c in let unfolded = try Tacred.try_red_product env sigma c - with _ -> error "fold: the term is not unfoldable !" + with e when Errors.noncritical e -> + error "fold: the term is not unfoldable !" in try let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in @@ -1072,7 +1077,7 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) - with _ -> None + with e when Errors.noncritical e -> None end @@ -1977,7 +1982,7 @@ let setoid_proof gl ty fn fallback = let evm = project gl in let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in fn env evm car rel gl - with e -> + with e when Errors.noncritical e -> try fallback gl with Hipattern.NoEquationFound -> match e with |