diff options
| author | herbelin | 2007-08-27 11:41:08 +0000 |
|---|---|---|
| committer | herbelin | 2007-08-27 11:41:08 +0000 |
| commit | c31fabdc5aadbf22d1d27f22aa737188acc6f12b (patch) | |
| tree | 5cbf70174b34c21cd771d9bcea1a6cdfa40a0c44 /contrib/correctness | |
| parent | 6b94d962f0722e218fa349651b6acd64c404bd29 (diff) | |
Suppression des type_app et body_of_type qui alourdissent inutilement le code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness')
| -rw-r--r-- | contrib/correctness/ptactic.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index e7610923cd..b99a3621d8 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -138,7 +138,7 @@ let (loop_ids : tactic) = fun gl -> then tclTHEN (clear [id]) (arec al) gl else if n >= 7 & String.sub s 0 7 = "Variant" then begin - match pf_matches gl eq_pattern (body_of_type a) with + match pf_matches gl eq_pattern a with | [_; _,varphi; _] when isVar varphi -> let phi = destVar varphi in if Termops.occur_var env phi concl then @@ -159,7 +159,6 @@ let (assumption_bis : tactic) = fun gl -> let rec arec = function | [] -> Util.error "No such assumption" | (s,a) :: al -> - let a = body_of_type a in if pf_conv_x_leq gl a concl then refine (mkVar s) gl else if pf_is_matching gl and_pattern a then |