diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/field/field.ml4 | 6 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 16 |
3 files changed, 17 insertions, 7 deletions
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index f08ed7db61..4ea9c99b79 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -154,7 +154,7 @@ let field g = | _ -> raise Exit with Hipattern.NoEquationFound | Exit -> error "The statement is not built from Leibniz' equality" in - let th = VConstr (lookup (pf_env g) typ) in + let th = VConstr ([],lookup (pf_env g) typ) in (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ()) <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g @@ -174,8 +174,8 @@ let field_term l g = Coqlib.check_required_library ["Coq";"field";"LegacyField"]; let env = (pf_env g) and evc = (project g) in - let th = valueIn (VConstr (guess_theory env evc l)) - and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in + let th = valueIn (VConstr ([],guess_theory env evc l)) + and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in (List.fold_right (fun c a -> let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 0f8c2f010b..4782e001a6 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -206,7 +206,7 @@ let exec_tactic env n f args = !res let constr_of = function - | VConstr c -> c + | VConstr ([],c) -> c | _ -> failwith "Ring.exec_tactic: anomaly" let stdlib_modules = diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 87c67cc147..80527f01d5 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -105,14 +105,24 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1)) else id - let pretype_id loc env (lvar,unbndltacvars) id = + let invert_ltac_bound_name env id0 id = + try mkRel (pi1 (lookup_rel_id id (rel_context env))) + with Not_found -> + errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ + str " depends on pattern variable name " ++ pr_id id ++ + str " which is not bound in current context") + + let pretype_id loc env sigma (lvar,unbndltacvars) id = let id = strip_meta id in (* May happen in tactics defined by Grammar *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> try - List.assoc id lvar + let (ids,c) = List.assoc id lvar in + let subst = List.map (invert_ltac_bound_name env id) ids in + let c = substl subst c in + { uj_val = c; uj_type = Retyping.get_type_of env sigma c } with Not_found -> try let (_,_,typ) = lookup_named id env in @@ -170,7 +180,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RVar (loc, id) -> inh_conv_coerce_to_tycon loc env evdref - (pretype_id loc env lvar id) + (pretype_id loc env !evdref lvar id) tycon | REvar (loc, ev, instopt) -> |