diff options
Diffstat (limited to 'plugins/ltac/taccoerce.ml')
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 58 |
1 files changed, 30 insertions, 28 deletions
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index df38a42cb..b76009c99 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -9,6 +9,7 @@ open Util open Names open Term +open EConstr open Pattern open Misctypes open Genarg @@ -17,7 +18,7 @@ open Geninterp exception CannotCoerceTo of string -let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) = +let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_context" in let () = register_val0 wit None in wit @@ -96,7 +97,7 @@ let is_variable env id = (* Transforms an id into a constr if possible, or fails with Not_found *) let constr_of_id env id = - Term.mkVar (let _ = Environ.lookup_named id env in id) + EConstr.mkVar (let _ = Environ.lookup_named id env in id) (* Gives the constr corresponding to a Constr_context tactic_arg *) let coerce_to_constr_context v = @@ -106,7 +107,7 @@ let coerce_to_constr_context v = else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) -let coerce_var_to_ident fresh env v = +let coerce_var_to_ident fresh env sigma v = let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then @@ -119,15 +120,16 @@ let coerce_var_to_ident fresh env v = | None -> fail () | Some c -> (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *) - if isVar c && not (fresh && is_variable env (destVar c)) then - destVar c + if isVar sigma c && not (fresh && is_variable env (destVar sigma c)) then + destVar sigma c else fail () (* Interprets, if possible, a constr to an identifier which may not be fresh but suitable to be given to the fresh tactic. Works for vars, constants, inductive, constructors and sorts. *) -let coerce_to_ident_not_fresh g env v = +let coerce_to_ident_not_fresh env sigma v = +let g = sigma in let id_of_name = function | Names.Anonymous -> Id.of_string "x" | Names.Name x -> x in @@ -143,7 +145,7 @@ let id_of_name = function match Value.to_constr v with | None -> fail () | Some c -> - match Constr.kind c with + match EConstr.kind sigma c with | Var id -> id | Meta m -> id_of_name (Evd.meta_name g m) | Evar (kn,_) -> @@ -162,14 +164,14 @@ let id_of_name = function basename | Sort s -> begin - match s with + match ESorts.kind sigma s with | Prop _ -> Label.to_id (Label.make "Prop") | Type _ -> Label.to_id (Label.make "Type") end | _ -> fail() -let coerce_to_intro_pattern env v = +let coerce_to_intro_pattern env sigma v = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then snd (out_gen (topwit wit_intro_pattern) v) @@ -177,14 +179,14 @@ let coerce_to_intro_pattern env v = let id = out_gen (topwit wit_var) v in IntroNaming (IntroIdentifier id) else match Value.to_constr v with - | Some c when isVar c -> + | Some c when isVar sigma c -> (* This happens e.g. in definitions like "Tac H = clear H; intro H" *) (* but also in "destruct H as (H,H')" *) - IntroNaming (IntroIdentifier (destVar c)) + IntroNaming (IntroIdentifier (destVar sigma c)) | _ -> raise (CannotCoerceTo "an introduction pattern") -let coerce_to_intro_pattern_naming env v = - match coerce_to_intro_pattern env v with +let coerce_to_intro_pattern_naming env sigma v = + match coerce_to_intro_pattern env sigma v with | IntroNaming pat -> pat | _ -> raise (CannotCoerceTo "a naming introduction pattern") @@ -232,7 +234,7 @@ let coerce_to_closed_constr env v = let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in c -let coerce_to_evaluable_ref env v = +let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in let v = Value.normalize v in let ev = @@ -253,8 +255,8 @@ let coerce_to_evaluable_ref env v = | IndRef _ | ConstructRef _ -> fail () else match Value.to_constr v with - | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) - | Some c when isVar c -> EvalVarRef (destVar c) + | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c)) + | Some c when isVar sigma c -> EvalVarRef (destVar sigma c) | _ -> fail () in if Tacred.is_evaluable env ev then ev else fail () @@ -266,14 +268,14 @@ let coerce_to_constr_list env v = List.map map l | None -> raise (CannotCoerceTo "a term list") -let coerce_to_intro_pattern_list loc env v = +let coerce_to_intro_pattern_list loc env sigma v = match Value.to_list v with | None -> raise (CannotCoerceTo "an intro pattern list") | Some l -> - let map v = (loc, coerce_to_intro_pattern env v) in + let map v = (loc, coerce_to_intro_pattern env sigma v) in List.map map l -let coerce_to_hyp env v = +let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then @@ -284,31 +286,31 @@ let coerce_to_hyp env v = let id = out_gen (topwit wit_var) v in if is_variable env id then id else fail () else match Value.to_constr v with - | Some c when isVar c -> destVar c + | Some c when isVar sigma c -> destVar sigma c | _ -> fail () -let coerce_to_hyp_list env v = +let coerce_to_hyp_list env sigma v = let v = Value.to_list v in match v with | Some l -> - let map n = coerce_to_hyp env n in + let map n = coerce_to_hyp env sigma n in List.map map l | None -> raise (CannotCoerceTo "a variable list") (* Interprets a qualified name *) -let coerce_to_reference env v = +let coerce_to_reference env sigma v = let v = Value.normalize v in match Value.to_constr v with | Some c -> begin - try Globnames.global_of_constr c + try fst (Termops.global_of_constr sigma c) with Not_found -> raise (CannotCoerceTo "a reference") end | None -> raise (CannotCoerceTo "a reference") (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) -let coerce_to_quantified_hypothesis v = +let coerce_to_quantified_hypothesis sigma v = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in @@ -321,17 +323,17 @@ let coerce_to_quantified_hypothesis v = else if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with - | Some c when isVar c -> NamedHyp (destVar c) + | Some c when isVar sigma c -> NamedHyp (destVar sigma c) | _ -> raise (CannotCoerceTo "a quantified hypothesis") (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) -let coerce_to_decl_or_quant_hyp env v = +let coerce_to_decl_or_quant_hyp env sigma v = let v = Value.normalize v in if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else - try coerce_to_quantified_hypothesis v + try coerce_to_quantified_hypothesis sigma v with CannotCoerceTo _ -> raise (CannotCoerceTo "a declared or quantified hypothesis") |