diff options
| author | Hugo Herbelin | 2015-11-08 09:54:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 08:58:20 +0100 |
| commit | 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 (patch) | |
| tree | fc399b19682aa528a73d90729c1e37ce4a761d6e /tactics | |
| parent | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (diff) | |
Moving three related small half-general half-ad-hoc utility functions
next to each other, waiting for possible integration into a more
uniform API.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 13 |
2 files changed, 3 insertions, 11 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index bf8f348551..ff1ed40301 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -19,6 +19,7 @@ open Tactics open Errors open Util open Evd +open Termops open Equality open Misctypes open Sigma.Notations diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4fb206ec94..a2275b08fb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -45,15 +45,6 @@ open Misctypes open Proofview.Notations open Sigma.Notations -let nb_prod x = - let rec count n c = - match kind_of_term c with - Prod(_,_,t) -> count (n+1) t - | LetIn(_,a,_,t) -> count n (subst1 a t) - | Cast(c,_,_) -> count n c - | _ -> n - in count 0 x - let inj_with_occurrences e = (AllOccurrences,e) let dloc = Loc.ghost @@ -1511,7 +1502,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) - let concl_nprod = nb_prod concl in + let concl_nprod = nb_prod_modulo_zeta concl in let rec try_main_apply with_destruct c = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in @@ -1520,7 +1511,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try - let n = nb_prod thm_ty - nprod in + let n = nb_prod_modulo_zeta thm_ty - nprod in if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags |