diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-13 00:16:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:17:24 +0200 |
| commit | 73cdb000ec07ec484557839c4b94fcf779df2f06 (patch) | |
| tree | 4aa04d713d26b537c187e1be801b4788d4a4e915 /proofs/logic.ml | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
Put the "clear" tactic into the monad.
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 09f308abe..df5a12473 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -636,16 +636,6 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution sigma goal oterm in (sgl, sigma) - (* And now the structural rules *) - | Thin ids -> - let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in - let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in - let (gl,ev,sigma) = - Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal) - in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in - ([gl], sigma) - | Move (hfrom, hto) -> let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in |