diff options
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 80c78c086..283de9ade 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -483,6 +483,7 @@ let start_proof_com sopt kind (bl,t) hook = let _ = Typeops.infer_type env c in start_proof id kind c hook +(* let apply_tac_not_declare id pft = function | None -> error "Type of Let missing" | Some typ -> @@ -490,6 +491,7 @@ let apply_tac_not_declare id pft = function and exat = Hiddentac.h_exact pft in Pfedit.delete_current_proof (); Pfedit.by (Refiner.tclTHENSV cutt [|introduction id;exat|]) +*) let save id const kind hook = let {const_entry_body = pft; |