diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 58 |
1 files changed, 1 insertions, 57 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f067141a8..a2caec7c5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -65,11 +65,6 @@ let skip_metaid = function | AI x -> x | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc -type ltac_type = - | LtacFun of ltac_type - | LtacBasic - | LtacTactic - (* Values for interpretation *) type value = | VRTactic of (goal list sigma) (* For Match results *) @@ -160,22 +155,6 @@ let valueOut = function (* To embed constr *) let constrIn t = CDynamic (dummy_loc,constr_in t) -let constrOut = function - | CDynamic (_,d) -> - if (Dyn.tag d) = "constr" then - constr_out d - else - anomalylabstrm "constrOut" (str "Dynamic tag should be constr") - | ast -> - anomalylabstrm "constrOut" (str "Not a Dynamic ast") - -(* Globalizes the identifier *) -let find_reference env qid = - (* We first look for a variable of the current proof *) - match repr_qualid qid with - | (d,id) when repr_dirpath d = [] & List.mem id (ids_of_context env) - -> VarRef id - | _ -> Nametab.locate qid (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty @@ -346,10 +325,6 @@ let intern_name l ist = function | Anonymous -> Anonymous | Name id -> Name (intern_ident l ist id) -let vars_of_ist (lfun,_,_,env) = - List.fold_left (fun s id -> Idset.add id s) - (vars_of_env env) lfun - let strict_check = ref false let adjust_loc loc = if !strict_check then dloc else loc @@ -519,12 +494,6 @@ let intern_bindings ist = function let intern_constr_with_bindings ist (c,bl) = (intern_constr ist c, intern_bindings ist bl) -let intern_clause_pattern ist (l,occl) = - let rec check = function - | (hyp,l) :: rest -> (intern_hyp ist (skip_metaid hyp),l)::(check rest) - | [] -> [] - in (l,check occl) - (* TODO: catch ltac vars *) let intern_induction_arg ist = function | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c) @@ -994,14 +963,6 @@ and intern_genarg ist x = (***************************************************************************) (* Evaluation/interpretation *) -let constr_to_id loc = function - | VConstr ([],c) when isVar c -> destVar c - | _ -> invalid_arg_loc (loc, "Not an identifier") - -let constr_to_qid loc c = - try shortest_qualid_of_global Idset.empty (global_of_constr c) - with _ -> invalid_arg_loc (loc, "Not a global reference") - let is_variable env id = List.mem id (ids_of_named_context (Environ.named_context env)) @@ -1149,16 +1110,6 @@ let interp_hyp_list_as_list ist gl (loc,id as x) = let interp_hyp_list ist gl l = List.flatten (List.map (interp_hyp_list_as_list ist gl) l) -let interp_clause_pattern ist gl (l,occl) = - let rec check acc = function - | (hyp,l) :: rest -> - let hyp = interp_hyp ist gl hyp in - if List.mem hyp acc then - error ("Hypothesis "^(string_of_id hyp)^" occurs twice."); - (hyp,l)::(check (hyp::acc) rest) - | [] -> [] - in (l,check [] occl) - let interp_move_location ist gl = function | MoveAfter id -> MoveAfter (interp_hyp ist gl id) | MoveBefore id -> MoveBefore (interp_hyp ist gl id) @@ -1396,8 +1347,6 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let interp_constr_list ist env sigma c = snd (interp_constr_in_compound_list (fun x -> x) (fun x -> x) (fun ist env sigma c -> (Evd.empty, interp_constr ist env sigma c)) ist env sigma c) -let inj_open c = (Evd.empty,c) - let interp_open_constr_list = interp_constr_in_compound_list (fun x -> x) (fun x -> x) (interp_open_constr None) @@ -2888,11 +2837,6 @@ and subst_genarg subst (x:glob_generic_argument) = (***************************************************************************) (* Tactic registration *) -(* For bad tactic calls *) -let bad_tactic_args s = - anomalylabstrm s - (str "Tactic " ++ str s ++ str " called with bad arguments") - (* Declaration of the TAC-DEFINITION object *) let add (kn,td) = mactab := Gmap.add kn td !mactab let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab) @@ -2937,7 +2881,7 @@ let subst_md (subst,(local,defs)) = let classify_md (local,defs as o) = if local then Dispose else Substitute o -let (inMD,outMD) = +let inMD = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; |