diff options
| author | herbelin | 2009-03-16 08:18:53 +0000 |
|---|---|---|
| committer | herbelin | 2009-03-16 08:18:53 +0000 |
| commit | 171c73b40b985f604e4d6c1529fb28d1dfa8e300 (patch) | |
| tree | ca36754a96d68fcedf329fb5217d41c171c30008 /contrib/funind | |
| parent | 208f162ab68d00488248ee052947592dd23d5d52 (diff) | |
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
etc.). The terminology for clauses (though I don't find the term
"clause" very intuitive after all) is mostly preserved except for
"simple_clause" which becomes a light form of "clause" instead of
being an atom of clause (what played the role of "simple_clause" is
now called "goal_location" - better names are welcome).
Main changes are in tacticals.ml and tactics.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/invfun.ml | 4 | ||||
| -rw-r--r-- | contrib/funind/recdef.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 5c8f087156..5f8587408b 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -565,11 +565,11 @@ let rec reflexivity_with_destruct_cases g = in let eq_ind = Coqlib.build_coq_eq () in let discr_inject = - Tacticals.onAllClauses ( + Tacticals.onAllHypsAndConcl ( fun sc g -> match sc with None -> tclIDTAC g - | Some ((_,id),_) -> + | Some id -> match kind_of_term (pf_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index aee133f6d9..a96ec6a438 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -1158,7 +1158,7 @@ let rec introduce_all_values_eq cont_tac functional termine simpl_iter (onHyp heq2); unfold_in_hyp [((true,[1]), evaluable_of_global_reference (global_of_constr functional))] - ((all_occurrences_expr, heq2), InHyp); + (heq2, InHyp); tclTHENS (fun gls -> let t_eq = compute_renamed_type gls (mkVar heq2) in |