aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
...
| | | * | | Tweak comments to fix ocamldoc errorsGravatar mrmr19932018-03-05
| |_|/ / / |/| | | |
* | | | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \
| | | | * | | Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| |_|_|/ / / |/| | | | |
| * | | | | tactics: export e_reduct_in_conclGravatar Enrico Tassi2018-03-04
| | | | | |
* | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ | |/ / / / / |/| | | | |
* | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | coretactics.ml4.
* \ \ \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \
| | | | | | | | * [compat] Remove "Standard Proposition Elimination"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Standard Proposition Elimination"
| | | | | | * | | [compat] Remove "Injection L2R Pattern Order"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | | | | | | |/ | | | | | | |/| | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Injection L2R Pattern Order".
| | | | * | / | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | |/ / | | | | |/| |
* | | | / | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | Noticed by Sigurd Schneider.
| | * | | | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
| |/ / / / |/| | | |
| | * | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag.
| | * | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ / |/| |
* | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
| * | proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
|/ /
* | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \
| | * Implement name mangling optionGravatar Jasper Hugunin2018-02-17
| | |
* | | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| |/ |/|
| * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
|/ | | | | | | | | | | | | | In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
|
* Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\
* \ Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \
| * | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
| | |
* | | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
|/ / | | | | | | | | | | | | | | | | | | | | Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt).
| * Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
| | | | | | | | | | | | | | We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy.
* | Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
|/ | | | | | This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
* Merge PR #6493: [API] remove large file containing duplicate interfacesGravatar Maxime Dénès2017-12-29
|\
| * [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
|/ | | | | | Some code in typeclasses was even breaking the invariant that use_polymorphic_flag should not be called twice, but that code was morally dead it seems, so we remove it.
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
* Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\
| * [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
| | | | | | | | | | We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
* | Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \
* | | | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair.
| | * Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| | | | | | | | | | | | And some code simplification.
| | * Remove deprecated option Dependent Propositions Eliminiation.Gravatar Théo Zimmermann2017-12-11
| |/ |/| | | | | And a bit of code simplification.
| * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* | Getting rid of pf_matches in Hipattern.Gravatar Pierre-Marie Pédrot2017-12-07
|/ | | | | | | | | | | Funnily enough, the old code is completely bogus. It succeeds in early files of the prelude just because the heterogeneous equality has not been required. This raises an exception which is not the same one as if we tried to rewrite with the identity type first. The only user, the inversion tactic, was actually only relying on Logic.eq and was furthermore not even using the convertibility algorithm. We just perform a syntactic match now.
* Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Gravatar Maxime Dénès2017-11-30
|\ | | | | | | #3125)
| * In injection/inversion, consider all template-polymorphic types as injectable.Gravatar Hugo Herbelin2017-11-28
| | | | | | | | | | | | | | In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273).
* | Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
* | When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
* | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
* | Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/
* Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Gravatar Maxime Dénès2017-11-24
|\ | | | | | | constructs.
| * Make one more function robust in term_dnet.mlGravatar Maxime Dénès2017-11-23
| | | | | | | | Was actually forgotten in native-coq.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 13:39:01 +0000