| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
for closed bugs
|
|
|
|
catched otherwise due to the discrepancy between evars and metas.
|
|
This commit should be refactored by Pierre L. if he thinks this should
replace the previous version of fold_Equal, for now it is a different
lemma fold_Equal2. Same for the Section addded to SetoiList, it should
maybe replace the previous one.
|
|
If the return predicate is not dependent, we avoid dynamically regenerating the
regular tree of the corresponding inductive type. This includes the commutative
cut rule. Should solve some performance issues observed in Compcert and Paco at
Qed time.
|
|
For better efficiency, we try to preserve the shape of mutually recursive
trees.
|
|
Used by the new guard criterion compatible with type isomorphisms.
|
|
|
|
|
|
|
