aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
|
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - 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
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
| | | | function, so plain pointer equality is sufficient.
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
| | | | Suggests in some cases the right bullet to use.
* Removing the call to Weak.get_copy in hashsets.Gravatar Pierre-Marie Pédrot2014-07-31
| | | | | | | | | | | | 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.
* micromega : refification recognises @eq T for T convertible with Z or RGravatar Frédéric Besson2014-07-31
|
* Typos.Gravatar Hugo Herbelin2014-07-31
|
* Finish fixes on notations and primitive projections, add test-suite files ↵Gravatar Matthieu Sozeau2014-07-31
| | | | for closed bugs
* Consistent pretty-printing of primitive projections and their expanded forms.Gravatar Matthieu Sozeau2014-07-31
|
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
| | | | catched otherwise due to the discrepancy between evars and metas.
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
| | | | | | | 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.
* Optimize check of new subterm relation on match.Gravatar Maxime Dénès2014-07-31
| | | | | | | 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.
* Improve intersection of regular trees.Gravatar Maxime Dénès2014-07-31
| | | | | For better efficiency, we try to preserve the shape of mutually recursive trees.
* Fix dynamic computation of recargs for mutual inductives.Gravatar Maxime Dénès2014-07-31
| | | | Used by the new guard criterion compatible with type isomorphisms.
* Add test-suite file for bug #3439.Gravatar Matthieu Sozeau2014-07-30
|
* Avoid hconsing instances during appends and conversions from/to arrays.Gravatar Matthieu Sozeau2014-07-30
|
* Fix discrimination net which was not recognizing primitive projections.Gravatar Matthieu Sozeau2014-07-30
|
* Avoid introducing additional universes when doing pruning in evarsolve.Gravatar Matthieu Sozeau2014-07-30
|
* CHANGES: untyped terms in tacticsGravatar Arnaud Spiwack2014-07-29
|
* Document untyped terms in tactics.Gravatar Arnaud Spiwack2014-07-29
|
* Small refactoring in Ltac parsing rules.Gravatar Arnaud Spiwack2014-07-29
|
* Allow [uconstr:c] as argument of a tactic.Gravatar Arnaud Spiwack2014-07-29
|
* Untyped terms in tactic: add the possibility to use a typed term inside an ↵Gravatar Arnaud Spiwack2014-07-29
| | | | untyped term.
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
|
* Untyped term in tactics: add an grammar entry to construct them.Gravatar Arnaud Spiwack2014-07-29
| | | | The syntax is uconstr:term.
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
| | | | | | It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
* Clean up obsolete comment.Gravatar Arnaud Spiwack2014-07-29
|
* Add test-suite file for bug 3454.Gravatar Matthieu Sozeau2014-07-29
|
* Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsGravatar Matthieu Sozeau2014-07-29
| | | | Specifications indicating that the record object must be a constructor. Fixes bug #3432.
* Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Gravatar Matthieu Sozeau2014-07-29
|
* Add test-suite file for bug #3453Gravatar Matthieu Sozeau2014-07-29
|
* Fix bug #3453, not recognizing primitive projections in Coercion declarations.Gravatar Matthieu Sozeau2014-07-29
|
* Fix treatment of notations containing applications of projections (fixes bug ↵Gravatar Matthieu Sozeau2014-07-29
| | | | #3454).
* STM: print goals with no duplicatesGravatar Enrico Tassi2014-07-29
|
* Pp: only one default feedback idGravatar Enrico Tassi2014-07-29
|
* Pp compiles after feedbackGravatar Enrico Tassi2014-07-29
|
* CPS-style tactic matching. We use the tactic monad as the target of the CPS.Gravatar Pierre-Marie Pédrot2014-07-28
| | | | | This allows for tail-rec calls, prevents unwanted capture of closures and results in an overall more efficient evaluation.
* Adding a tclBREAK primitive to the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-28
|
* Code cleaning in Tacenv.Gravatar Pierre-Marie Pédrot2014-07-27
|
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
| | | | potentially conflicting tactics names from different plugins.
* Removing dead code relative to or_metaid.Gravatar Pierre-Marie Pédrot2014-07-25
|
* CHANGES: cycle and swap.Gravatar Arnaud Spiwack2014-07-25
|
* Document swap tactic.Gravatar Arnaud Spiwack2014-07-25
|
* Document cycle tactic.Gravatar Arnaud Spiwack2014-07-25
|
* Add a tactic [swap i j] to swap the position of goals [i] and [j].Gravatar Arnaud Spiwack2014-07-25
| | | If [i] or [j] is negative goals are counted from the end.
* Adds a cycle tactic to reorder goals in a loop.Gravatar Arnaud Spiwack2014-07-25
| | | [cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].
* A slightly more fine grained way to check whether a TACTIC EXTEND is global ↵Gravatar Arnaud Spiwack2014-07-25
| | | | | or local to goals. Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global.
* CHANGES: yellow in Coqide.Gravatar Arnaud Spiwack2014-07-25
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 22:40:31 +0000