diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-05 15:56:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-09 16:04:42 +0200 |
| commit | 68a7940b2d6b03fd511faf8ad8a65edc9f7aa0e1 (patch) | |
| tree | 281501dd118cd87dfc6d0b90d6062971920c5ad6 /proofs/logic.ml | |
| parent | e824d429363262a9ff9db117282fe15289b5ab59 (diff) | |
Removing Convert_concl and Convert_hyp from Logic.
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 2d302510e..3be202476 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -655,20 +655,6 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution sigma goal oterm in (sgl, sigma) - (* Conversion rules *) - | Convert_concl (cl',k) -> - check_typability env sigma cl'; - let (sg,ev,sigma) = mk_goal sign cl' in - let sigma = check_conv_leq_goal env sigma cl' cl' cl in - let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in - let sigma = Goal.V82.partial_solution_to sigma goal sg ev in - ([sg], sigma) - - | Convert_hyp (id,copt,ty) -> - let (gl,ev,sigma) = mk_goal (convert_hyp !check sign sigma (id,copt,ty)) cl in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in - ([gl], 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 |