diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-29 19:23:25 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-29 19:23:25 +0000 |
| commit | b20e1be71f9b5c5585b214e30b5042676fa6cd46 (patch) | |
| tree | 6e9b6b6078d69420ee90751377d2f015fd8f1323 /tactics/tacentries.ml | |
| parent | 50457d3bf6aee2a49dd9c0acf7389b885178ea3f (diff) | |
Ajout du Let pour le langage de tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacentries.ml')
| -rw-r--r-- | tactics/tacentries.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml index f7afda327..852b0ff83 100644 --- a/tactics/tacentries.ml +++ b/tactics/tacentries.ml @@ -14,8 +14,6 @@ let v_transitivity = hide_tactic "Transitivity" dyn_transitivity let v_intro = hide_tactic "Intro" dyn_intro let v_intro_move = hide_tactic "IntroMove" dyn_intro_move let v_introsUntil = hide_tactic "IntrosUntil" dyn_intros_until -(*i let v_tclIDTAC = hide_tactic "Idtac" dyn_tclIDTAC -let v_tclFAIL = hide_tactic "Fail" dyn_tclFAIL i*) let v_assumption = hide_tactic "Assumption" dyn_assumption let v_exact = hide_tactic "Exact" dyn_exact_check let v_reduce = hide_tactic "Reduce" dyn_reduce |