From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 18 Jan 2010 09:51:09 +0000 (+0000)
Subject: Number notation for NG
X-Git-Tag: make_still_working~3116
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=52a0d6251f26055df769b179641fe077046e1f09;p=helm.git

Number notation for NG
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 6aee803f4..28742e6c7 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -81,12 +81,18 @@ let ncic_mk_choice = function
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
-       let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
-       desc, `Num_interp
+     (try
+       let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
+        desc, `Num_interp
+         (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
+      with
+       DisambiguateChoices.Choice_not_found _ ->
+        let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
+        desc, `Num_interp
          (fun num -> 
             fst (OCic2NCic.convert_term 
               (UriManager.uri_of_string "cic:/xxx/x.con") 
-              (match f with `Num_interp f -> f num | _ -> assert false)))
+              (match f with `Num_interp f -> f num | _ -> assert false))))
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 68299b8ea..7be30e407 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -483,6 +483,7 @@ EXTEND
   auto_fixed_param: [
    [ IDENT "paramodulation"
    | IDENT "fast_paramod"
+   | IDENT "paramod"
    | IDENT "slir"
    | IDENT "depth"
    | IDENT "width"