diff options
| author | barras | 2003-11-13 18:02:09 +0000 |
|---|---|---|
| committer | barras | 2003-11-13 18:02:09 +0000 |
| commit | 9aab7ae10aa1d535734f336c4bce16d908576d65 (patch) | |
| tree | 34c92bbeaae2cc973dfbec48d921eae6934d9cdc /translate | |
| parent | 4c18a78b54ff33361990a6f19bcad69bb7a4417c (diff) | |
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Local devient Let
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 4 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 4 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index f708f12d1d..33d6ce7861 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -40,8 +40,8 @@ let lfix = 200 let larrow = 90 let lcast = 100 let lapp = 10 -let lposint = 1 (* above the argument of notation "- x" *) -let lnegint = lapp (* above application *) +let lposint = 0 +let lnegint = 35 (* must be consistent with Notation "- x" *) let ltop = (200,E) let lproj = 1 let lsimple = (1,E) diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 491076b0be..72d4a56082 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -492,13 +492,13 @@ and pr_atom1 env = function pr_clauses pr_ident cls)) (* Derived basic tactics *) | TacSimpleInduction h -> - hov 1 (str "simple_induction" ++ pr_arg pr_quantified_hypothesis h) + hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) | TacNewInduction (h,e,ids) -> hov 1 (str "induction" ++ spc () ++ pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++ pr_opt (pr_eliminator env) e) | TacSimpleDestruct h -> - hov 1 (str "simple_destruct" ++ pr_arg pr_quantified_hypothesis h) + hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) | TacNewDestruct (h,e,ids) -> hov 1 (str "destruct" ++ spc () ++ pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++ diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 9162049688..9e6aa0fe05 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -581,7 +581,7 @@ let rec pr_vernac = function let pr_def_token = function | Local, Coercion -> str"Coercion Local" | Global, Coercion -> str"Coercion" - | Local, Definition -> str"Local" + | Local, Definition -> str"Let" | Global, Definition -> str"Definition" | Local, SubClass -> str"Local SubClass" | Global, SubClass -> str"SubClass" |