diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:28:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:28:49 +0000 |
| commit | cd4d18cf0de8e8077a9c141a3e825b7647f03f8e (patch) | |
| tree | bb87d0c21994886b468ca468a0a30ba1bb675e3c | |
| parent | 4b71b4bfc7b5a0316f549a88fa6495acde9d27c5 (diff) | |
Code mort ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3391 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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; |