Monomorphization (parsing)

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

5 files changed, 14 insertions, 11 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index dd32c99ba..1c00e6581 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -177,7 +177,10 @@ let pure_sublevels level symbs =
   let filter s =
     try
       let i = level_of_snterml s in
-      if level = Some i then None else Some i
+      begin match level with
+      | Some j when Int.equal i j -> None
+      | _ -> Some i
+      end
     with Failure _ -> None
   in
   List.map_filter filter symbs
@@ -289,7 +292,7 @@ let extend_grammar gram =
 
 let recover_notation_grammar ntn prec =
   let filter = function
-  | _, Notation (prec', vars, ng) when prec = prec' & ntn = ng.notgram_notation ->
+  | _, Notation (prec', vars, ng) when Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation ->
     Some (vars, ng)
   | _ -> None in
   let l = List.map_filter filter !grammar_state in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 40eb78cdc..af6699867 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -359,13 +359,13 @@ GEXTEND Gram
   ;
   simple_assum_coe:
     [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
-        (oc <> None,(idl,c)) ] ]
+        (not (Option.is_empty oc),(idl,c)) ] ]
   ;
 
   constructor_type:
     [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
-	            fun l id -> (coe <> None,(id,mkCProdN (!@loc) l c))
+	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN (!@loc) l c))
             |  ->
 		 fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None)))) ]
 	 -> t l
@@ -612,7 +612,7 @@ GEXTEND Gram
            | [] -> narg, impl in
          let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in
          let nargs, rest = List.hd nargs, List.tl nargs in
-         if List.exists ((<>) nargs) rest then
+         if List.exists (fun arg -> not (Int.equal arg nargs)) rest then
            error "All arguments lists must have the same length";
          let err_incompat x y =
            error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
@@ -677,7 +677,7 @@ GEXTEND Gram
   ;
   argument_spec: [
        [ b = OPT "!"; id = name ; s = OPT scope ->
-       snd id, b <> None, Option.map (fun x -> !@loc, x) s
+       snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s
     ]
   ];
   strategy_level:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 377da0bdf..e1a43c400 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -30,7 +30,7 @@ type attribute = string * (Loc.t * string)
 type xml = XmlTag of Loc.t * string * attribute list * xml list
 
 let check_tags loc otag ctag =
-  if otag <> ctag then
+  if not (String.equal otag ctag) then
     user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
       str "does not match open xml tag " ++ str otag ++ str ".")
 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 80940b4d3..4b3a3f3a1 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -131,7 +131,7 @@ let utf8_char_size cs = function
 let njunk n = Util.repeat n Stream.junk
 
 let check_utf8_trailing_byte cs c =
-  if Char.code c land 0xC0 <> 0x80 then error_utf8 cs
+  if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 cs
 
 (* Recognize utf8 blocks (of length less than 4 bytes) *)
 (* but don't certify full utf8 compliance (e.g. no emptyness check) *)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 66b248cb0..b7d2c844f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -116,7 +116,7 @@ module Gramtypes : Gramtypes =
 struct
   let inGramObj rawwit = in_typed_entry (unquote rawwit)
   let outGramObj (a:'a raw_abstract_argument_type) o =
-    if type_of_typed_entry o <> unquote a
+    if not (argument_type_eq (type_of_typed_entry o) (unquote a))
       then anomaly "outGramObj: wrong type";
     (* downcast from grammar_object *)
     Obj.magic (object_of_typed_entry o)
@@ -162,7 +162,7 @@ let grammar_delete e reinit (pos,rls) =
     (fun (n,ass,lev) ->
       List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
     (List.rev rls);
-  if reinit <> None then
+  if reinit != None then
     let lev = match pos with Some (Level n) -> n | _ -> assert false in
     let pos = match lev with
     | "200" -> First
@@ -279,7 +279,7 @@ let new_entry etyp (u, utab) s =
 let create_entry (u, utab) s etyp =
   try
     let e = Hashtbl.find utab s in
-    if type_of_typed_entry e <> etyp then
+    if not (argument_type_eq (type_of_typed_entry e) etyp) then
       failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
     e
   with Not_found ->