aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2014-11-20Probably useless use of a global-environment reading function in Indrec.Pierre-Marie Pédrot
2014-11-19Making map_union a standard function of the ML library.Hugo Herbelin
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-19Continuing fixing nested but convertible occurrences in find_subtermHugo Herbelin
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-19uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...Arnaud Spiwack
2014-11-19Glob-ops: a name-mapping operation for pattern-matching binders.Arnaud Spiwack
2014-11-18Fixing a little bug with nested but convertible occurrences in "destruct at".Hugo Herbelin
2014-11-18Fixing detection of occurrences in the presence of nested subterms forHugo Herbelin
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-14Get rif of exit codes 120, 121, 123, and 124.Xavier Clerc
2014-11-11Accepting conversion on inner closed subterms while looking forHugo Herbelin
2014-11-10Evar normalization is now done eagerly.Pierre-Marie Pédrot
2014-11-09Fixing bug #3792.Pierre-Marie Pédrot
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-11-08Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Hugo Herbelin
2014-11-04Experimentally applying eager evar substitution at the same time asHugo Herbelin
2014-11-03Fixing confused code for interpretations of evar instances.Hugo Herbelin
2014-11-03Fixing inefficiency in typeclass resolution.Pierre-Marie Pédrot
2014-11-02Fixing subterm matched for destruct when it is matched from prefix.Hugo Herbelin
2014-11-02Cosmetic changes.Hugo Herbelin
2014-11-02Fixing 1177da327 (reorganization of the test for generic selection ofHugo Herbelin
2014-10-31Reorganization of the test for generic selection of occurrences inHugo Herbelin
2014-10-31Enlarge the cases where the like first selection is used in destruct.Hugo Herbelin
2014-10-27Removing dead code from Evd.Pierre-Marie Pédrot
2014-10-27Removing the Evd.diff function.Pierre-Marie Pédrot
2014-10-27Removing the Evd.merge function.Pierre-Marie Pédrot
2014-10-27Dead codeHugo Herbelin
2014-10-26Applying like-first selection for destruct in hypotheses.Hugo Herbelin
2014-10-26Fixing destruct/induction with a using clause on a non-inductive type,Hugo Herbelin
2014-10-26Dead code + typo.Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-24Fixing order of hypothesis in goal hypotheses compaction for coqtop.Hugo Herbelin
2014-10-23Fixing order of declarations in the function which compacts variablesHugo Herbelin
2014-10-22Pushing Pierre's factorization of names in goal context printing fromHugo Herbelin
2014-10-22Removing an unused variant of Context.fold_named_context_reverse.Hugo Herbelin
2014-10-22Fix missing lift in VM and native compiler (second part of #2729).Maxime Dénès
2014-10-22Fixing an evar leak in pattern-matching compilation (#3758).Hugo Herbelin
2014-10-22Add more primitives to the [Monad.Make] arguments.Arnaud Spiwack
2014-10-21Porting Hugo's fix 98f3abb83a to native compiler.Maxime Dénès
2014-10-21Dead code.Hugo Herbelin
2014-10-20Fixing a (new) part of bug #2729.Hugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-20Fixing a bug in the presence of let-in in inductive arity.Hugo Herbelin
2014-10-17When facing problem ?id = ?id' in resolution of return predicate,Hugo Herbelin
2014-10-17New experimental heuristic printing strategy for evar instances: WeHugo Herbelin
2014-10-17Re-displaying evar instances in debugger.Hugo Herbelin
2014-10-16Refine: proper scoping of the future goals.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 22:36:02 +0000