diff options
| author | Hugo Herbelin | 2014-10-05 15:56:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-09 16:04:42 +0200 |
| commit | 68a7940b2d6b03fd511faf8ad8a65edc9f7aa0e1 (patch) | |
| tree | 281501dd118cd87dfc6d0b90d6062971920c5ad6 /proofs/proof_type.ml | |
| parent | e824d429363262a9ff9db117282fe15289b5ab59 (diff) | |
Removing Convert_concl and Convert_hyp from Logic.
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 2f0b0e6083..925aff10ef 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -32,8 +32,6 @@ type prim_rule = | FixRule of Id.t * int * (Id.t * int * constr) list * int | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr - | Convert_concl of types * cast_kind - | Convert_hyp of named_declaration | Thin of Id.t list | Move of bool * Id.t * Id.t move_location | Rename of Id.t * Id.t |