From 56f2bee1436eef74d3ddb1ae36ae00e5ddae16bd Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 12 Apr 2012 17:28:13 +0000 Subject: remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15129 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/subtac/subtac.ml | 227 ----------------------------------------------- 1 file changed, 227 deletions(-) delete mode 100644 plugins/subtac/subtac.ml (limited to 'plugins') diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml deleted file mode 100644 index a8d69bdcfc..0000000000 --- a/plugins/subtac/subtac.ml +++ /dev/null @@ -1,227 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constant_value (Global.env()) - (match cst with ConstRef kn -> kn | _ -> assert false) - | _ -> - 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 (loc,id) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"start_proof",pr_id id ++ str " already exists"); - id - | None -> - next_global_ident_away (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) - in - let evm, c, typ, imps = - Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None - in - let c = solve_tccs_in_type env id isevars evm c typ in - Lemmas.start_proof id kind c (fun loc gr -> - Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps]; - hook loc gr) - -let start_proof_and_print env isevars idopt k t hook = - start_proof_com env isevars idopt k t hook; - Vernacentries.print_subgoals () - -let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) - -let assumption_message id = - Flags.if_verbose message ((string_of_id id) ^ " is assumed") - -let declare_assumptions env isevars idl is_coe k bl c nl = - if not (Pfedit.refining ()) then - let id = snd (List.hd idl) in - let evm, c, typ, imps = - Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None - in - let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_assumption is_coe k c imps false nl) idl - else - errorlabstrm "Command.Assumption" - (str "Cannot declare an assumption while in proof editing mode.") - -let dump_constraint ty ((loc, n), _, _) = - match n with - | Name id -> Dumpglob.dump_definition (loc, id) false ty - | Anonymous -> () - -let dump_variable lid = () - -let vernac_assumption env isevars kind l nl = - let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> - if Dumpglob.dump () then - List.iter (fun lid -> - if global then Dumpglob.dump_definition lid (not global) "ax" - else dump_variable lid) idl; - declare_assumptions env isevars idl is_coe kind [] c nl) l - -let check_fresh (loc,id) = - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"",pr_id id ++ str " already exists") - -let subtac (loc, command) = - check_required_library ["Coq";"Init";"Datatypes"]; - check_required_library ["Coq";"Init";"Specif"]; - let env = Global.env () in - let isevars = ref (create_evar_defs Evd.empty) in - try - match command with - | VernacDefinition (defkind, (_, id as lid), expr, hook) -> - check_fresh lid; - Dumpglob.dump_definition lid false "def"; - (match expr with - | ProveBody (bl, t) -> - start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) - (fun _ _ -> ()) - | DefineBody (bl, _, c, tycon) -> - ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) - | 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) - - | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> - if guard <> None then - error "Do not support building theorems as a fixpoint."; - Dumpglob.dump_definition id false "prf"; - if not(Pfedit.refining ()) then - if lettop then - errorlabstrm "Subtac_command.StartProof" - (str "Let declarations can only be used in proof editing mode"); - if Lib.is_modtype () then - errorlabstrm "Subtac_command.StartProof" - (str "Proof editing mode not supported in module types"); - check_fresh id; - start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook - - | VernacAssumption (stre,nl,l) -> - vernac_assumption env isevars stre l nl - - | VernacInstance (abst, glob, sup, is, props, pri) -> - dump_constraint "inst" is; - if abst then - error "Declare Instance not supported here."; - ignore(Subtac_classes.new_instance ~global:glob sup is props pri) - - | VernacCoFixpoint l -> - if Dumpglob.dump () then - List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; - ignore(Subtac_command.build_corecursive l) - - (*| VernacEndProof e -> - subtac_end_proof e*) - - | _ -> user_err_loc (loc,"", str ("Invalid Program command")) - with - | Typing_error e -> - msg_warning (str "Type error in Program tactic:"); - let cmds = - (match e with - | NonFunctionalApp (loc, x, mux, e) -> - str "non functional application of term " ++ - e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux - | NonSigma (loc, t) -> - str "Term is not of Sigma type: " ++ t - | NonConvertible (loc, x, y) -> - str "Unconvertible terms:" ++ spc () ++ - x ++ spc () ++ str "and" ++ spc () ++ y - | IllSorted (loc, t) -> - str "Term is ill-sorted:" ++ spc () ++ t - ) - in msg_warning cmds - - | Subtyping_error e -> - msg_warning (str "(Program tactic) Subtyping error:"); - let cmds = - match e with - | UncoercibleInferType (loc, x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - | UncoercibleInferTerm (loc, x, y, tx, ty) -> - str "Uncoercible terms:" ++ spc () - ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x - ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y - | UncoercibleRewrite (x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - in msg_warning cmds - - | Cases.PatternMatchingError (env, exn) as e -> raise e - - | Type_errors.TypeError (env, exn) as e -> raise e - - | Pretype_errors.PretypeError (env, _, exn) as e -> raise e - - | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | - Loc.Exc_located (loc, e') as e) -> raise e - - | e -> - (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *) - raise e -- cgit v1.2.3