Rustine pour gérer inject_nat

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1954 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 3 deletions

diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 62fd1796e..12c7e017c 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -64,6 +64,7 @@ with expr0 : constr :=
 
 with application : constr :=
   apply [ application($p) expr($c1) ] -> [ ($p $c1) ]
+| apply_inject_nat [ "inject_nat" constr:constr($c1) ] -> [ (inject_nat $c1) ]
 | pair [ expr($p) "," expr($c) ] -> [ ($p, $c) ]
 | appl0 [ expr($a) ] -> [$a]
 .
@@ -155,6 +156,8 @@ Syntax constr
   level 4:
     Zappl_inside [ << (ZEXPR (APPLIST $h ($LIST $t))) >> ]
       -> [ [<hov 0> "("(ZEXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E ")"] ]
+  | Zappl_inject_nat [ << (ZEXPR (APPLIST <<inject_nat>> $n)) >> ]
+      -> [ (APPLIST <<inject_nat>> $n) ]
   | Zappl_inside_tail [ << (APPLINSIDETAIL $h ($LIST $t)) >> ]
       -> [(ZEXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E] 
   | Zappl_inside_one [ << (APPLINSIDETAIL $e) >> ] ->[(ZEXPR $e):E]
@@ -169,9 +172,10 @@ Syntax constr
       -> [(MUTIND $i $n)]
   | mutconstruct_inside [ << (ZEXPR (MUTCONSTRUCT $c1 $c2 $c3)) >> ]
       -> [ (MUTCONSTRUCT $c1 $c2 $c3) ]
-  (* Added by JCF, 9/3/98 *)
-  | implicit_head_inside [ << (ZEXPR (XTRA "!" $c)) >> ] -> [ $c ]
-  | implicit_arg_inside  [ << (ZEXPR (XTRA "!" $n $c)) >> ] -> [ ]
+  (* Added by JCF, 9/3/98; updated HH, 11/9/01 *)
+  | implicit_head_inside [ << (ZEXPR (APPLISTEXPL ($LIST $c))) >> ]
+      -> [ (APPLIST ($LIST $c)) ]
+  | implicit_arg_inside  [ << (ZEXPR (EXPL "!" $n $c)) >> ] -> [ ]
 
   ;