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_obligations.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_obligations.ml')
-rw-r--r-- | plugins/subtac/subtac_obligations.ml | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index d61ca2bc8..3d1e836a7 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -184,12 +184,11 @@ let declare_definition prg = my_print_constr (Global.env()) body ++ str " : " ++ my_print_constr (Global.env()) prg.prg_type); with _ -> ()); - let (local, boxed, kind) = prg.prg_kind in + let (local, kind) = prg.prg_kind in let ce = { const_entry_body = body; const_entry_type = Some typ; - const_entry_opaque = false; - const_entry_boxed = boxed} + const_entry_opaque = false } in (Command.get_declare_definition_hook ()) ce; match local with @@ -207,7 +206,7 @@ let declare_definition prg = | (Global|Local) -> let c = Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind)) + prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind)) in let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then @@ -255,7 +254,7 @@ let declare_mutual_definition l = let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in - let (local,boxed,kind) = first.prg_kind in + let (local,kind) = first.prg_kind in let fixnames = first.prg_deps in let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in let indexes, fixdecls = @@ -269,7 +268,7 @@ let declare_mutual_definition l = None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l in (* Declare the recursive definitions *) - let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in + let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames; @@ -288,8 +287,7 @@ let declare_obligation prg obl body = let ce = { const_entry_body = body; const_entry_type = Some ty; - const_entry_opaque = opaque; - const_entry_boxed = false} + const_entry_opaque = opaque } in let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) @@ -557,7 +555,7 @@ let show_term n = my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ my_print_constr (Global.env ()) prg.prg_body) -let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic +let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in @@ -575,7 +573,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) +let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) ?(hook=fun _ _ -> ()) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left |