| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.
This fixes #6313.
Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Adding also tclSETSHELF/tclGETSHELF by consistency with
tclSETGOALS/tclGETGOALS.
However, I feel that this is too low-level to be exported as a
"tcl". Doesn't a "tcl" mean that it is supposed to be used by common
tactics? But is it reasonable that a common tactic can change and
modify comb and shelf without passing by a level which e.g. checks
that no goal is lost in the process.
So, I would rather be in favor of removing tclSETGOALS/tclGETGOALS
which are anyway aliases for Comb.get/Comb.set.
Conversely, what is the right expected level of abstraction for
proofview.ml?
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | | |
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | | |
Following up on #6791, we remove the option "Standard Proposition Elimination"
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | | |
|
| | |/ /
|/| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ / |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| |/
|
|
|
|
|
|
|
|
| |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
| |\
| |
| |
| | |
error msg
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The type discipline of the tactic monad does not distinguish between
mono-goal and multi-goal tactics. Unfortunately enter_one "asserts
false" if called on 0 or > 1 goals. The __LOC__:string argument can
be used to make the error message more helpful (since the backtrace is
pointless inside the monad).
The intended usage is "Goal.enter_one ~__LOC__ (fun gl -> ..".
The __LOC__ variable is filled in by the OCaml compiler with the current
file name and line number.
|
| |\ \ |
|
| |\ \ \
| |_|/
|/| | |
|
| | | | |
|
| |\ \ \
| |/ /
|/| | |
|
| |\ \ \ |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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).
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |/
|/|
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | |/ / /
| | | | |
| | | | |
| | | | | |
These are also convenient from `vernac` [to be used in future PRs].
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Thanks to @SkySkimmer for lots of comments and bug-finding.
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
Hugo Herbelin
Maxime Dénès
Gaëtan Gilbert
mrmr1993
Enrico Tassi
Emilio Jesus Gallego Arias
Théo Zimmermann
Pierre-Marie Pédrot
Jasper Hugunin
Cyprien Mangin