| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
| |
Substitution of the Ltac variables would only occur if the internalised [uconstr] was of the form [glob, Some expr], which is the case only in tactics defined inside a proof, but not in tactics defined in [Ltac].
|
| |
|
| |
Arguments of refine can hence be built by tactics instead of given in their entirety in one go.
|
| |
|
|
| |
grammar rules.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.
|
| |
|
|
|
| |
When dynamically computing the recarg tree, we now prune it according to the
inferred tree. Compilation of CompCert is now ok.
|
| |
|
|
|
| |
I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Remove proofview_gen, which was the repository of the extracted code, and move it to proofview_monad, which has the actual interface used by the [Proofview] module to implement tactics.
|
| |
|
|
|
|
|
|
|
| |
* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v
|
| | |
|
| |
|
|
|
| |
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
|
| |
|
|
| |
- Decomment code in reductionops forgotten after debugging.
|
| |
|
|
|
|
|
| |
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
| |
|
|
|
|
| |
- Allow apply's unification to use conversion even if some polymorphic
constants appear in the goal (consistent with occur_meta_or_evar, and
evarconv in general).
|
| |
|
|
|
| |
explicitly or implicitly to the variables in the as and in clauses +
formatting.
|
| | |
|
| | |
|
| |
|
| |
Detyping was called on every typed constr in the Ltac context which was costly as most of the context is likely not to be refered to in a particular uconstr. This commit calls detyping lazily instead.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
Differs from the usual t;[t1…tn] in two ways:
* It can be used without a preceding tactic
* It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals.
In other words t;[t1…tn] is [> t;[>t1…tn].. ].
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails.
Together with [numgoal] can be used to fork on the number of goals of a tactic.
The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility.
|
| | |
|
| |
|
|
| |
The [num_goal] tactic counts the number of focused goals.
|
| |
|
|
| |
Following advice by Hugo Herbelin.
|
| |
|
|
| |
Introduced in a4043608f
|
| | |
|
| | |
|
| |
|
|
| |
* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
|
| | |
|
| |
|
|
|
| |
* unused terms are generalised
* proof is abstract
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
|
| | |
|
| | |
|
| |
|
|
| |
function, so plain pointer equality is sufficient.
|
| |
|
|
| |
Suggests in some cases the right bullet to use.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The rationale for its use comes from OCaml weak maps, and is justified by the
fact that Weak.get may prevent its return value to be collected by the GC during
the next slice even though nobody points to it. In our case, this is vastly
irrelevant because hashconsed values are not expected to be collected whatsoever
(save for exceptional cases). But Weak.get_copy is rather costly actually, at
least strictly more than the plain Weak.get.
Experimentally, I observe diminution of compilation time and even diminution
of memory consumption (!) after this patch, so I assume it is a net gain.
|
Arnaud Spiwack
Pierre Boutillier
Maxime Dénès
Pierre-Marie Pédrot
Carst Tankink
Enrico Tassi
Matthieu Sozeau
Hugo Herbelin
Frédéric Besson
Pierre Courtieu