diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-19 10:06:11 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-19 10:06:11 +0000 |
commit | 6a6fc7ec30f0fb48d9cfef379f9cab0fa8fffb39 (patch) | |
tree | 1678fb26f64eddb97949ff63a38d240182cb4ce0 /pretyping/tacred.ml | |
parent | 2435a02751df1818977ce58ddf21a8f12ed87be6 (diff) |
Arguments/simpl: allow ! even on non fixpoints
It is now possible to tell simpl to unfold a constant
that hides no "match" but is applied to concrete arguments.
Arguments id _ !n.
Goal forall x, id x = id 2.
intros; simpl.
x : nat
========
id x = 2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15048 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r-- | pretyping/tacred.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 13b2ddcaa..4e45fb226 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -611,9 +611,9 @@ let dont_expose_case r = let rec red_elim_const env sigma ref largs = let nargs = stack_args_size largs in - let largs, unfold_anyway = + let largs, unfold_anyway, unfold_nonelim = match recargs ref with - | None -> largs, false + | None -> largs, false, false | Some (_,n) when nargs < n -> raise Redelimination | Some (l,n) -> List.fold_left (fun stack i -> @@ -622,7 +622,8 @@ let rec red_elim_const env sigma ref largs = match kind_of_term (fst rarg) with | Construct _ -> stack_assign stack i (app_stack rarg) | _ -> raise Redelimination) - largs l, n >= 0 && l = [] && nargs >= n in + largs l, n >= 0 && l = [] && nargs >= n, + n >= 0 && l <> [] && nargs >= n in try match reference_eval sigma env ref with | EliminationCases n when nargs >= n -> let c = reference_value sigma env ref in @@ -652,6 +653,9 @@ let rec red_elim_const env sigma ref largs = (match reduce_fix_use_function env sigma f whfun (destFix d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta sigma c, rest)) + | NotAnElimination when unfold_nonelim -> + let c = reference_value sigma env ref in + whd_betaiotazeta sigma (app_stack (c, largs)), empty_stack | _ -> raise Redelimination with Redelimination when unfold_anyway -> let c = reference_value sigma env ref in |