From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jun 2016 18:25:02 +0200 Subject: Moving the typing_flags to the environment. --- plugins/funind/indfun.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8b3d3dc20f..0cacb003d8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint ~flags:Declareops.safe_flags Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> -- cgit v1.2.3