aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
Commit message (Collapse)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [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
|/
* pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Gravatar Enrico Tassi2018-02-19
|
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
| * Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
|/ | | | Also nicer error when the constraints are impossible.
* [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | Note the problem with `create_evar_defs`.
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
* Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| | | | | When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
* Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
| | | | Use the functional interface understand_tcc instead.
* Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
|
* Remove understand_judgment and understand_judgment_tcc.Gravatar Maxime Dénès2017-08-01
|
* Remove allow_anonymous_refs.Gravatar Maxime Dénès2017-08-01
|
* Remove pure_open_constr (now open_constr)Gravatar Maxime Dénès2017-08-01
|
* Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
| | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
| * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
| |
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ | | | Now it is a private field, locations are optional.
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | We make mli files look to what they were looking before the move to EConstr by opening this module.
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Fix bug #4723 and FIXME in API for solve_by_tacGravatar Matthieu Sozeau2016-09-28
| | | | | | | | | | | | This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic.
* | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
| |
* | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
|/
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
|
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
| | | | | | | | | | | | | | | | | | This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper.
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
| |
* | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
| |
* | Adding location to universes generated by the pretyper.Gravatar Pierre-Marie Pédrot2016-02-19
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
* | | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
| | |
* | | Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
|/ /
* | Documenting a bit more interpretation functions in passing.Gravatar Hugo Herbelin2015-10-26
| |
* | Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | capturing bound names unexpectingly). We moved renaming to after finding bindings, i.e. in pretyping "fun x y => x + y" in an ltac environment where y is ltac-bound to x, we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1" (which later on is displayed into "fun y y0 => y + y0"). We renounced to renaming in "match" patterns, which was anyway not working well, as e.g. in let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0). which was producing forall z : nat, match z with 0 => z | S y => y end = 0 because the names in default branches are treated specifically. It would be easy to support renaming in match again, by putting the ltac env in the Cases.pattern_matching_problem state and to rename the names in "typs" (from build_branch), just before returning them at the end of the function (and similarly in abstract_predicate for the names occurring in the return predicate). However, we rename binders in fix which were not interpreted. There are some difficulties with evar because we want them defined in the interpreted env (see comment to ltac_interp_name_env). fix ltac name
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
|