diff options
| author | msozeau | 2008-09-03 14:47:14 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-03 14:47:14 +0000 |
| commit | 73e85bb97b86c53f34b984d0193835c1d722c59f (patch) | |
| tree | b899bd39dae595bce1e0433d2dfb5c75bc73aae4 | |
| parent | d1372d531ff912fe726ed4a79ac556d378a37375 (diff) | |
Better handling of recursive Equations definitions... still not perfect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11356 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/subtac/equations.ml4 | 1 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 21 |
2 files changed, 16 insertions, 6 deletions
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4 index 4464d1ca63..14330e72eb 100644 --- a/contrib/subtac/equations.ml4 +++ b/contrib/subtac/equations.ml4 @@ -666,6 +666,7 @@ let define_by_eqs i l t nt eqs = let prob = (i, sign, arity) in let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in let ce = check_evars fixenv Evd.empty !isevar in + List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; let is_recursive, env' = let occur_eqn (ctx, _, rhs) = match rhs with diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 2bf25c8e70..d11996a672 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -408,10 +407,10 @@ Ltac simplify_method H := clear H ; simplify_dep_elim ; reverse. (** Solving a method call: we must refine the goal until the body can be applied or just solve it by splitting on an empty family member. *) -Ltac solve_method := +Ltac solve_method rec := match goal with | [ H := ?body : nat |- _ ] => simplify_method H ; solve_empty body - | [ H := ?body |- _ ] => simplify_method H ; (try intro) ; try_intros body + | [ H := ?body |- _ ] => simplify_method H ; rec ; try_intros body end. (** Impossible cases, by splitting on a given target. *) @@ -429,9 +428,19 @@ Ltac intro_prototypes := | _ => idtac end. +Ltac nonrec_equations := + solve [solve_equations (solve_method idtac)] || solve [ solve_split ] + || fail "Unnexpected equations goal". + +Ltac recursive_equations := + solve [solve_equations (solve_method ltac:intro)] || solve [ solve_split ] + || fail "Unnexpected recursive equations goal". + (** The [equations] tactic is the toplevel tactic for solving goals generated by [Equations]. *) -Ltac equations := intro_prototypes ; - solve [solve_equations solve_method] || solve [ solve_split ] || fail "Unnexpcted equations goal". - +Ltac equations := + match goal with + | [ |- Π x : _, _ ] => intro ; recursive_equations + | _ => nonrec_equations + end. |