Take notations into account: numbers and the CNotation operator.

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

6 files changed, 21 insertions, 15 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 983cd68d9..fb9d6476b 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -223,10 +223,10 @@ and ct_FORMULA =
   | CT_elimc of ct_CASE * ct_FORMULA * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
-  | CT_incomplete_binary of ct_FORMULA * ct_BINARY
-  | CT_int_encapsulator of ct_INT
+  | CT_int_encapsulator of string
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
   | CT_letin of ct_ID_OPT * ct_FORMULA * ct_FORMULA
+  | CT_notation of ct_STRING * ct_FORMULA_LIST
   | CT_prodc of ct_BINDER_NE_LIST * ct_FORMULA
 and ct_FORMULA_LIST =
     CT_formula_list of ct_FORMULA list
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 26026b6cd..854c76db4 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -2,8 +2,6 @@ open Util;;
 
 open System;;
 
-open Ctast;;
-
 open Pp;;
 
 open Libnames;;
@@ -108,6 +106,7 @@ let execute_when_necessary ast =
 let execute_when_necessary v =
  (match v with
   | VernacGrammar _ -> Vernacentries.interp v
+  | VernacOpenScope sc -> Vernacentries.interp v
   | VernacRequire (_,_,l) ->
       (try 
 	Vernacentries.interp v
@@ -280,7 +279,7 @@ let parse_string_action reqid phylum char_stream string_list =
       | "FORMULA" ->
        P_f
         (xlate_formula
-        (Ctast.ast_to_ct (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream))))
+	   (Gram.Entry.parse Pcoq.Constr.constr_eoi (Gram.parsable char_stream)))
       | "ID" -> P_id (xlate_ident
                        (Gram.Entry.parse Pcoq.Prim.ident
                               (Gram.parsable char_stream)))
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index fe6be23b2..effa9aca0 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -577,14 +577,9 @@ and fFORMULA = function
    fID x1;
    fFIX_BINDER_LIST x2;
    fNODE "fixc" 2
-| CT_incomplete_binary(x1, x2) ->
-   fFORMULA x1;
-   fBINARY x2;
-   fNODE "incomplete_binary" 2
-| CT_int_encapsulator(x1) ->
-   fINT x1;
-   fNODE "int_encapsulator" 1
-| CT_lambdac(x1, x2) ->
+| CT_int_encapsulator x -> fATOM "int_encapsulator";
+   (f_atom_string x);
+   print_string "\n"| CT_lambdac(x1, x2) ->
    fBINDER_NE_LIST x1;
    fFORMULA x2;
    fNODE "lambdac" 2
@@ -593,6 +588,10 @@ and fFORMULA = function
    fFORMULA x2;
    fFORMULA x3;
    fNODE "letin" 3
+| CT_notation(x1, x2) ->
+   fSTRING x1;
+   fFORMULA_LIST x2;
+   fNODE "notation" 2
 | CT_prodc(x1, x2) ->
    fBINDER_NE_LIST x1;
    fFORMULA x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 480293333..1ba580c45 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -280,7 +280,9 @@ let xlate_qualid a =
   let l = Names.repr_dirpath d in
   List.fold_left (fun s i1 -> (string_of_id i1) ^ "." ^ s) (string_of_id i) l;;
    
-
+(* // The next two functions should be modified to make direct reference
+  to a notation operator *)
+let notation_to_formula s l = CT_notation(CT_string s, CT_formula_list l);;
 
 let xlate_reference = function
     Ident(_,i) -> CT_ident (string_of_id i)
@@ -319,6 +321,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CApp(_, f, l) ->
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
+   | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
+   | CNumeral(_, i) -> CT_int_encapsulator(Bignat.bigint_to_string i)
    | _ -> assert false
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
@@ -1405,7 +1409,7 @@ let xlate_vernac =
    | VernacFixpoint [] -> xlate_error "mutual recursive"
    | VernacFixpoint (lm :: lmi) ->
       let strip_mutrec (fid, n, arf, ardef) =
-        let (bl,arf,ardef) = Ppconstr.split_fix n arf ardef in
+        let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match cvt_fixpoint_binders bl with
diff --git a/lib/bignat.ml b/lib/bignat.ml
index bac879644..348b1225b 100644
--- a/lib/bignat.ml
+++ b/lib/bignat.ml
@@ -111,3 +111,6 @@ let pr_bigint = function
   | POS n -> str (to_string n)
   | NEG n -> str "-" ++ str (to_string n)
 
+let bigint_to_string = function
+  | POS n -> to_string n
+  | NEG n -> "-" ^ (to_string n);;
diff --git a/lib/bignat.mli b/lib/bignat.mli
index d901f556f..ca2b0fff6 100644
--- a/lib/bignat.mli
+++ b/lib/bignat.mli
@@ -33,4 +33,5 @@ val less_than : bignat -> bignat -> bool
 
 type bigint = POS of bignat | NEG of bignat
 
+val bigint_to_string : bigint -> string
 val pr_bigint : bigint -> std_ppcmds