| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a reimplementation of Hugo's PR#117.
We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.
Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.
We renamed the following functions:
Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
And removed the following ones:
Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta
They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).
Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.
Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
The tentative fix in f9695eb4b (which I was afraid it might be too
strong, since it was implying failing more often) indeed broke other
things (see #4813).
|
| | |
| |
| |
| |
| |
| | |
Trying to now catch all unification errors, but without a clear view
at whether some errors could be tolerated at the point of checking the
type of the binding.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | |
| |
| |
| |
| |
| |
| | |
Return the most appropriate evar_map for commands that can run on
non-focused proofs (like Check, Show and debug printers) so that
universes and existentials are printed correctly (they are global
to the proof). The API is backwards compatible.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
The "Classic" string is still hard coded here in there in the system, but
not in STM.
BTW, the use of an hard coded "Classic" value suggests nobody really uses
"Set Default Proof Mode" in .v files.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This fix is too restrictive. Still, opening a goal for an evar with a
pending conv_pb is unsafe since the user may prove (instantiate it) in
a way not compatible with the conv_pb.
Assigning an evar, in its lowest level API, should enforce that all
related conv_pbs are satisfied by the instance.
This also poses a UI problem, since there is not way to see these
conv_pbs. One could print a goal and say: look, the proof term you give
must validate this equation...
Given that the good fix is not obvious, we revert!
This reverts commit a0e792236c9666df1069753f8f807c12f713dcfb.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This fixes a class of bugs like
refine foo; tactic.
where tactic fails (by resuming the remaining, unsolvable, problems) while
in 8.4 refine was failing.
It is not clear to us (Maxime and myself) if we should call
consider_remaining_unif_problems instead of check_problems_are_solved.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Instead of mangling the AST in order to interpret par: we remember the goal
position to focus on it first and evaluate then the underlying vernacular
expression.
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| |\| |
|
| | |
| |
| |
| |
| | |
The environment put in the goals was not the right one and could lead to
various leaks.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
I propose to change the name of the "Util.compose" function to "%".
Reasons:
1. If one wants to express function composition,
then the new name enables us to achieve this goal easier.
2. In "Batteries Included" they had made the same choice.
|
| |/| | |
|
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Pierre Letouzey
Cyprien Mangin
Emilio Jesus Gallego Arias
Matthieu Sozeau
Enrico Tassi
Matthieu Sozeau
Matej Kosik