diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-17 18:25:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
| commit | 53ced0735f7e24735d78a02fc74588b8d9186eab (patch) | |
| tree | 93661920f42d9be934e59f5f972d165ea24785b7 /toplevel/vernacentries.ml | |
| parent | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (diff) | |
Moving the typing_flags to the environment.
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5131a4179..29d6d7acd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -576,17 +576,17 @@ let vernac_inductive chk poly lo finite indl = let indl = List.map unpack indl in do_mutual_inductive chk indl poly lo finite -let vernac_fixpoint ~flags locality poly local l = +let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_fixpoint ~flags local poly l + do_fixpoint local poly l -let vernac_cofixpoint ~flags locality poly local l = +let vernac_cofixpoint locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_cofixpoint ~flags local poly l + do_cofixpoint local poly l let vernac_scheme l = if Dumpglob.dump () then @@ -1731,8 +1731,6 @@ let vernac_load interp fname = try while true do interp (snd (parse_sentence input)) done with End_of_input -> () -let all_checks = Declareops.safe_flags - (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. @@ -1770,8 +1768,8 @@ let interp ?proof ~loc locality poly c = | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l - | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l - | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l + | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l + | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l | VernacUniverse l -> vernac_universe loc poly l |