aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2013-02-17A more informative message when the elimination predicate forherbelin
2013-02-17Locating errors from consider_remaining_unif_problems if possibleherbelin
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-10Splitted Evarutil in two filesppedrot
2013-02-10Moved code from Pretype_error to Evarutilppedrot
2013-02-05Revert "Ordered evars by level of dependency in the merging phase of unificat...herbelin
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Fixing one part of #2830 (anomaly "defined twice" due to nested calls toherbelin
2013-01-28Added backtrace information to anomaliesppedrot
2013-01-27Ordered evars by level of dependency in the merging phase of unificationherbelin
2013-01-27Improving formatting of output of "Test table".herbelin
2013-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2013-01-22- Fix evarconv so that we have complete eta-conversion:msozeau
2013-01-18Evarconv: Check stack before term in Canonical Structure approuvalpboutill
2012-12-21Awful heuristic to refold mutual fixpoint in reductionopspboutill
2012-12-21Fixup and comment reductionopspboutill
2012-12-19Reductionops reduction machine can refold constantpboutill
2012-12-19Evarconv.Pseudorigid erasurepboutill
2012-12-19Array.create is deprecatedpboutill
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-18Taking into account the possibility of having a type of type which isherbelin
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-18Factorization of the elim unif flag with the default flag. Sinceherbelin
2012-12-17Do not display REVERTcast inserted by reduction tactics (unless printing all).herbelin
2012-12-17Fixed a bug in the algorithm trying to elaborate a "match" return predicate.herbelin
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-11-28Evarconv: Fix #2936 + commentspboutill
2012-11-28Reductionops uses Closure.redspboutill
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-26Small cleaning of interface in Univppedrot
2012-11-25More equality functionsppedrot
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
2012-11-23Added a constr_pattern_eqppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-20Cleaning and small optimization in CList.ppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-11-08Removing another bunch of generic equalitiesppedrot
2012-11-03Reversed roles of undefined/defined evars in Evd, thus saving preciousppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 09:01:28 +0000