aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-03-13A bit of cleaning: unifying push_rels and push_rel_context.herbelin
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-03-02Noise for nothingpboutill
2012-03-01Univ: a univ_depends function to avoid a hack in Inductiveopsletouzey
2012-02-15Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...msozeau
2012-01-31Bug #2041: unfold at betaiotaZETA normalize like unfoldpboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2012-01-27Printing bugs with match patterns:herbelin
2012-01-23Fix for Program Instance not separately checking the resolution of evars of t...msozeau
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-12-18Continuing 14812 and 14813 (use type information to reduce theherbelin
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-12-17Added ability to take the type of applied metas into account whenherbelin
2011-12-17Reorganizing Unification.unify_0 so as to more easily share codeherbelin
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
2011-12-06Backtrack on synchronizing universe counter with resetherbelin
2011-12-05Registering universe and meta/evar counters as summaries so as toherbelin
2011-12-05Yet another fix about alias in testing if pattern unification applies.herbelin
2011-12-04Fixed a small regression in pattern-matching compilation introduced inherbelin
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
2011-11-28Finally used typing to decide whether an alias needs to be expanded orherbelin
2011-11-28Fixing dependencies postprocessing bug in pattern-matching compilation.herbelin
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-25avoid relying on weak invariant in cbv.mlbgregoir
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-23Adds a pair of function in Evar_util to gather dependent evars in anaspiwack
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-21Configurable simpl tacticgareuselesinge
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-21Add matching on non-inductive types in building an inversion problemherbelin
2011-11-21Old naming bug in pattern-matching compilation: names in theherbelin
2011-11-21Inlining let-in (i.e. trace of aliases) in extract_predicate for whatherbelin
2011-11-21In pattern-matching compilation, now taking into account the dependenciesherbelin
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
2011-11-21Simplifying history management in pattern-matching compilation.herbelin
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
2011-11-21Removing stuff about alias dependencies now become useless.herbelin
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
2011-11-21Dead code + refreshing some comments in cases.ml.herbelin
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-18Fix for subclasses implementation, allowing to register generalized classes s...msozeau
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 02:42:40 +0000