summaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:10 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:10 +0200
commit499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /tactics/rewrite.ml4
parentbf12eb93f3f6a6a824a10878878fadd59745aae0 (diff)
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'tactics/rewrite.ml4')
-rw-r--r--tactics/rewrite.ml425
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