diff options
-rw-r--r-- | proofs/logic.ml | 7 | ||||
-rw-r--r-- | tactics/tactics.ml | 10 |
2 files changed, 13 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 74a1cf762..013cf227f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -393,9 +393,10 @@ let convert_hyp sign sigma (id,b,bt as d) = apply_to_hyp sign id (fun sign (_,c,ct) _ -> let env = Global.env_of_context sign in - if !check && not (is_conv env sigma bt ct) && - not (option_compare (is_conv env sigma) b c) then - error "convert-hyp rule passed non-converting term"; + if !check && not (is_conv env sigma bt ct) then + error ("Incorrect change of the type of "^(string_of_id id)); + if !check && not (option_compare (is_conv env sigma) b c) then + error ("Incorrect change of the body of "^(string_of_id id)); add_named_decl d sign) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0216b3b65..81fba94c7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -225,8 +225,16 @@ let pattern_option l = reduct_option (pattern_occs l) (* A function which reduces accordingly to a reduction expression, as the command Eval does. *) +let needs_check = function + (* Expansion is not necessarily well-typed: e.g. expansion of t into x is + not well-typed in [H:(P t); x:=t |- G] because x is defined after H *) + | Fold _ -> true + | _ -> false + let reduce redexp cl goal = - redin_combinator (Redexpr.reduction_of_red_expr redexp) cl goal + (if needs_check redexp then with_check else (fun x -> x)) + (redin_combinator (Redexpr.reduction_of_red_expr redexp) cl) + goal (* Unfolding occurrences of a constant *) |