Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 5 insertions, 1 deletions

diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5b45a8dbed..13ff19a46b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -106,6 +106,7 @@ let change_vars =
       | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported")
       | GSort _ as x -> x
       | GHole _ as x -> x
+      | GInt _ as x -> x
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
                 Glob_ops.map_cast_type (change_vars mapping) c)
@@ -285,6 +286,7 @@ let rec alpha_rt excluded rt =
 	   )
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GSort _
+    | GInt _
     | GHole _ as rt -> rt
     | GCast (b,c) ->
 	GCast(alpha_rt excluded b,
@@ -344,6 +346,7 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
+    | GInt _ -> false
     ) x
   and is_free_in_br {CAst.v=(ids,_,rt)} =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -434,6 +437,7 @@ let replace_var_by_term x_id term =
       | GRec _ -> raise (UserError(None,str "Not handled GRec"))
       | GSort _
       | GHole _ as rt -> rt
+      | GInt _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
                 Glob_ops.map_cast_type replace_var_by_pattern c)
@@ -516,7 +520,7 @@ let expand_as =
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map = DAst.map (function
-      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt
+      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt
       | GVar id as rt ->
 	  begin
 	    try