diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-05 21:50:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-15 20:21:37 +0200 |
| commit | dcf4d3e28813e09fc71f974b79ddf42d2e525976 (patch) | |
| tree | 76a95699918b818e3f6111b594b5b6ec7bd566b2 /toplevel | |
| parent | 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 (diff) | |
Remove the syntax changes introduced by this branch.
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 40dfa1b9a..a5e771d75 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1856,6 +1856,7 @@ let vernac_load interp fname = try while true do interp (snd (parse_sentence input)) done with End_of_input -> () +let all_checks = { Declarations.check_guarded = true } (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands @@ -1894,9 +1895,9 @@ let interp ?proof locality poly c = | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl - | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l - | VernacFixpoint (flags,local, l) -> vernac_fixpoint ~flags locality poly local l - | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags locality poly local l + | 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 | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l | VernacUniverse l -> vernac_universe l |