aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Get rif of exit codes 120, 121, 123, and 124.Gravatar Xavier Clerc2014-11-14
* Accepting conversion on inner closed subterms while looking forGravatar Hugo Herbelin2014-11-11
* Evar normalization is now done eagerly.Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing bug #3792.Gravatar Pierre-Marie Pédrot2014-11-09
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Gravatar Hugo Herbelin2014-11-08
* Experimentally applying eager evar substitution at the same time asGravatar Hugo Herbelin2014-11-04
* Fixing confused code for interpretations of evar instances.Gravatar Hugo Herbelin2014-11-03
* Fixing inefficiency in typeclass resolution.Gravatar Pierre-Marie Pédrot2014-11-03
* Fixing subterm matched for destruct when it is matched from prefix.Gravatar Hugo Herbelin2014-11-02
* Cosmetic changes.Gravatar Hugo Herbelin2014-11-02
* Fixing 1177da327 (reorganization of the test for generic selection ofGravatar Hugo Herbelin2014-11-02
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Removing dead code from Evd.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.diff function.Gravatar Pierre-Marie Pédrot2014-10-27
* Removing the Evd.merge function.Gravatar Pierre-Marie Pédrot2014-10-27
* Dead codeGravatar Hugo Herbelin2014-10-27
* Applying like-first selection for destruct in hypotheses.Gravatar Hugo Herbelin2014-10-26
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* Dead code + typo.Gravatar Hugo Herbelin2014-10-26
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Fixing order of hypothesis in goal hypotheses compaction for coqtop.Gravatar Hugo Herbelin2014-10-24
* Fixing order of declarations in the function which compacts variablesGravatar Hugo Herbelin2014-10-23
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* Removing an unused variant of Context.fold_named_context_reverse.Gravatar Hugo Herbelin2014-10-22
* Fix missing lift in VM and native compiler (second part of #2729).Gravatar Maxime Dénès2014-10-22
* Fixing an evar leak in pattern-matching compilation (#3758).Gravatar Hugo Herbelin2014-10-22
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
* Porting Hugo's fix 98f3abb83a to native compiler.Gravatar Maxime Dénès2014-10-21
* Dead code.Gravatar Hugo Herbelin2014-10-21
* Fixing a (new) part of bug #2729.Gravatar Hugo Herbelin2014-10-20
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Fixing a bug in the presence of let-in in inductive arity.Gravatar Hugo Herbelin2014-10-20
* When facing problem ?id = ?id' in resolution of return predicate,Gravatar Hugo Herbelin2014-10-17
* New experimental heuristic printing strategy for evar instances: WeGravatar Hugo Herbelin2014-10-17
* Re-displaying evar instances in debugger.Gravatar Hugo Herbelin2014-10-17
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* Move the handling a new evars from the [Proofview.Refine] module to [Evd].Gravatar Arnaud Spiwack2014-10-16
* Evd: a few comments to document the increasingly wide internal [evar_map] type.Gravatar Arnaud Spiwack2014-10-16
* Evd: remove/update obsolete comments.Gravatar Arnaud Spiwack2014-10-16
* To stay closer to non-primitive projections, only unfold primitiveGravatar Matthieu Sozeau2014-10-15
* Make use of unfolded primitive projections when elaborating match on aGravatar Matthieu Sozeau2014-10-15
* Fix bug 3637.Gravatar Matthieu Sozeau2014-10-15
* Reenable FO unification of primitive projections and their eta-expandedGravatar Matthieu Sozeau2014-10-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 12:50:59 +0000