diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/dune | 8 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 16 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 12 |
3 files changed, 21 insertions, 15 deletions
diff --git a/plugins/ltac/dune b/plugins/ltac/dune index 6558ecbfe8..9ec2b10873 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -1,15 +1,15 @@ (library (name ltac_plugin) - (public_name coq.plugins.ltac) + (public_name coq-core.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) - (libraries coq.stm)) + (libraries coq-core.stm)) (library (name tauto_plugin) - (public_name coq.plugins.tauto) + (public_name coq-core.plugins.tauto) (synopsis "Coq's tauto tactic") (modules tauto) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6d0e0c36b3..c7bda43465 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -251,10 +251,10 @@ end) = struct (** Folding/unfolding of the tactic constants. *) - let unfold_impl sigma t = + let unfold_impl n sigma t = match EConstr.kind sigma t with | App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) -> - mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b) + mkProd (make_annot n Sorts.Relevant, a, lift 1 b) | _ -> assert false let unfold_all sigma t = @@ -273,16 +273,16 @@ end) = struct | _ -> assert false) | _ -> assert false - let arrow_morphism env evd ta tb a b = + let arrow_morphism env evd n ta tb a b = let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in - if ap && bp then app_poly env evd impl [| a; b |], unfold_impl + if ap && bp then app_poly env evd impl [| a; b |], unfold_impl n else if ap then (* Domain in Prop, CoDomain in Type *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (make_annot n Sorts.Relevant, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n let rec decomp_pointwise sigma n c = if Int.equal n 0 then c @@ -1079,7 +1079,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let arr = if prop then PropGlobal.arrow_morphism else TypeGlobal.arrow_morphism in - let (evars', mor), unfold = arr env evars tx tb x b in + let (evars', mor), unfold = arr env evars n.binder_name tx tb x b in let state, res = aux { state ; env ; unfresh ; term1 = mor ; ty1 = ty ; cstr = (prop,cstr) ; evars = evars' } in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f2241e78d2..54d7c310aa 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2148,7 +2148,8 @@ let interp_redexp env sigma r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let eval lfun poly env sigma ty tac = + let eval ?loc ~poly env sigma tycon tac = + let lfun = GlobEnv.lfun env in let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = eval_tactic_ist ist tac in @@ -2156,8 +2157,13 @@ let _ = poly seems like enough to get reasonable behavior in practice *) let name = Id.of_string "ltac_gen" in - let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in - (EConstr.of_constr c, sigma) + let sigma, ty = match tycon with + | Some ty -> sigma, ty + | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) + in + let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in + let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in + (j, sigma) in GlobEnv.register_constr_interp0 wit_tactic eval |