diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 3 |
4 files changed, 9 insertions, 5 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f549adf7ae..700beaff59 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -339,7 +339,9 @@ let generate_functional_principle { const_entry_body = value; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false + } in ignore( Declare.declare_constant diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 7785cbe592..a74ae84e24 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -409,7 +409,7 @@ let is_free_in id = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> false | GHole _ -> false - | GCast (_,b,(CastConv t|CastVM t)) -> is_free_in b || is_free_in t + | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (_,b,CastCoerce) -> is_free_in b and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt @@ -590,7 +590,7 @@ let ids_of_glob_constr c = | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCast (loc,c,(CastConv t|CastVM t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc | GLetTuple (_,nal,(na,po),b,c) -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e662cd41d1..4b87a9b9cc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -60,7 +60,8 @@ let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = let ce = {const_entry_body = value; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false } in + const_entry_opaque = false; + const_entry_inline_code = false} in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_named false diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index c89e06f7c2..3bb57a3b36 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -147,7 +147,8 @@ let decl_constant na c = { const_entry_body = c; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = true }, + const_entry_opaque = true; + const_entry_inline_code = false}, IsProof Lemma)) (* Calling a global tactic *) |