diff options
author | 2011-01-28 13:20:41 +0000 | |
---|---|---|
committer | 2011-01-28 13:20:41 +0000 | |
commit | f19a9d9d3a410fda982b2cf9154da5774f9ec84f (patch) | |
tree | 23e166d4564ec1382afb60ec0d03e976dcaff377 /plugins/subtac/subtac.ml | |
parent | c7fb97fd915a732e1d91ca59fd635c95235052ce (diff) |
Remove the "Boxed" syntaxes and the const_entry_boxed field
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/subtac.ml')
-rw-r--r-- | plugins/subtac/subtac.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index e614085e4..fbdaa8d3b 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -141,12 +141,12 @@ let subtac (loc, command) = (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) - | VernacFixpoint (l, b) -> + | VernacFixpoint l -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; Dumpglob.dump_definition lid false "fix") l; let _ = trace (str "Building fixpoint") in - ignore(Subtac_command.build_recursive l b) + ignore(Subtac_command.build_recursive l) | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> if guard <> None then @@ -171,10 +171,10 @@ let subtac (loc, command) = error "Declare Instance not supported here."; ignore(Subtac_classes.new_instance ~global:glob sup is props pri) - | VernacCoFixpoint (l, b) -> + | VernacCoFixpoint l -> if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; - ignore(Subtac_command.build_corecursive l b) + ignore(Subtac_command.build_corecursive l) (*| VernacEndProof e -> subtac_end_proof e*) |