diff options
Diffstat (limited to 'contrib/subtac/subtac.ml')
| -rw-r--r-- | contrib/subtac/subtac.ml | 52 |
1 files changed, 34 insertions, 18 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 4f5e302c2..56ebc4f52 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -49,6 +49,22 @@ open Decl_kinds open Tacinterp open Tacexpr +let solve_tccs_in_type env id isevars evm c typ = + if not (evm = Evd.empty) then + let stmt_id = Nameops.add_suffix id "_stmt" in + let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in + (** Make all obligations transparent so that real dependencies can be sorted out by the user *) + let obls = Array.map (fun (id, t, op, d) -> (id, t, false, d)) obls in + match Subtac_obligations.add_definition stmt_id c' typ obls with + Subtac_obligations.Defined cst -> constant_value (Global.env()) cst + | _ -> + errorlabstrm "start_proof" + (str "The statement obligations could not be resolved automatically, " ++ spc () ++ + str "write a statement definition first.") + else + let _ = Typeops.infer_type env c in c + + let start_proof_com env isevars sopt kind (bl,t) hook = let id = match sopt with | Some id -> @@ -60,21 +76,11 @@ let start_proof_com env isevars sopt kind (bl,t) hook = next_global_ident_away false (id_of_string "Unnamed_thm") (Pfedit.get_all_proof_names ()) in - let evm, c, typ = + let evm, c, typ, _imps = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None in - if not (evm = Evd.empty) then - let stmt_id = Nameops.add_suffix id "_stmt" in - let obls, c' = eterm_obligations env stmt_id !isevars evm 0 c (Some typ) in - match Subtac_obligations.add_definition stmt_id c' typ obls with - Subtac_obligations.Defined cst -> Command.start_proof id kind (constant_value (Global.env()) cst) hook - | _ -> - errorlabstrm "start_proof" - (str "The statement obligations could not be resolved automatically, " ++ spc () ++ - str "write a statement definition first.") - else - let _ = Typeops.infer_type env c in - Command.start_proof id kind c hook + let c = solve_tccs_in_type env id isevars evm c typ in + Command.start_proof id kind c hook let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () @@ -88,10 +94,12 @@ let assumption_message id = Flags.if_verbose message ((string_of_id id) ^ " is assumed") let declare_assumption env isevars idl is_coe k bl c nl = - if not (Pfedit.refining ()) then - let evm, c, typ = - Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None + if not (Pfedit.refining ()) then + let id = snd (List.hd idl) in + let evm, c, typ, imps = + Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None in + let c = solve_tccs_in_type env id isevars evm c typ in List.iter (Command.declare_one_assumption is_coe k c nl) idl else errorlabstrm "Command.Assumption" @@ -114,8 +122,13 @@ let subtac (loc, command) = match command with VernacDefinition (defkind, (locid, id), expr, hook) -> (match expr with - ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None) - | DefineBody (bl, _, c, tycon) -> + | ProveBody (bl, t) -> + if Lib.is_modtype () then + errorlabstrm "Subtac_command.StartProof" + (str "Proof editing mode not supported in module types"); + start_proof_and_print env isevars (Some id) (Global, DefinitionBody Definition) (bl,t) + (fun _ _ -> ()) + | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon)) | VernacFixpoint (l, b) -> let _ = trace (str "Building fixpoint") in @@ -135,6 +148,9 @@ let subtac (loc, command) = | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl + | VernacInstance (sup, is, props) -> + Subtac_classes.new_instance sup is props + (* | VernacCoFixpoint (l, b) -> *) (* let _ = trace (str "Building cofixpoint") in *) (* ignore(Subtac_command.build_recursive l b) *) |