diff options
| author | Pierre-Marie Pédrot | 2016-06-20 08:40:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-20 08:53:39 +0200 |
| commit | b0ffad7f20114875611132dfffb9517d6f5b9ff9 (patch) | |
| tree | 7b9eef41c1d081e1ab21aad510d03c5ad3b77641 | |
| parent | a7d95a6923960ad551314d3e72715f9ad766cffd (diff) | |
Small optimization in clear_body.
We do not check that an hypothesis is used in context declarations that
occur before it.
| -rw-r--r-- | tactics/tactics.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d4158d7872..c336bb434a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2026,16 +2026,18 @@ let clear_body ids = let env = push_named_context ctx base_env in let check = try - let check (env, sigma) decl = + let check (env, sigma, seen) decl = (** Do no recheck hypotheses that do not depend *) let sigma = - if List.exists (fun id -> occur_var_in_decl env id decl) ids then + if not seen then sigma + else if List.exists (fun id -> occur_var_in_decl env id decl) ids then check_decl env sigma decl else sigma in - (push_named decl env, sigma) + let seen = seen || List.mem_f Id.equal (get_id decl) ids in + (push_named decl env, sigma, seen) in - let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in + let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in let sigma = if List.exists (fun id -> occur_var env id concl) ids then check_is_type env sigma concl |