aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Impossible branches inference fixup (bug 2761)Gravatar pboutill2012-05-11
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Revise API of understand_ltac to be parameterized by a flag for resolution of...Gravatar msozeau2012-03-14
* Merge fixesGravatar msozeau2012-03-14
* Everything compiles again.Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* A bit of cleaning: unifying push_rels and push_rel_context.Gravatar herbelin2012-03-13
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
* Noise for nothingGravatar pboutill2012-03-02
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
* Fixed a small regression in pattern-matching compilation introduced inGravatar herbelin2011-12-04
* Finally used typing to decide whether an alias needs to be expanded orGravatar herbelin2011-11-28
* Fixing dependencies postprocessing bug in pattern-matching compilation.Gravatar herbelin2011-11-28
* Fixed a bug in postprocessing dependencies in pattern-matching compilationGravatar herbelin2011-11-26
* Extend the computation of dependencies in pattern-matching compilationGravatar herbelin2011-11-21
* Add matching on non-inductive types in building an inversion problemGravatar herbelin2011-11-21
* Old naming bug in pattern-matching compilation: names in theGravatar herbelin2011-11-21
* Inlining let-in (i.e. trace of aliases) in extract_predicate for whatGravatar herbelin2011-11-21
* In pattern-matching compilation, now taking into account the dependenciesGravatar herbelin2011-11-21
* Optimizing the compilation of unused aliases in pattern-matching.Gravatar herbelin2011-11-21
* Simplifying history management in pattern-matching compilation.Gravatar herbelin2011-11-21
* Fixing postprocessing bugs in pattern-matching compilation.Gravatar herbelin2011-11-21
* Removing stuff about alias dependencies now become useless.Gravatar herbelin2011-11-21
* Changed the way to detect if an "as" patterns is expanded or not. TheGravatar herbelin2011-11-21
* Dead code + refreshing some comments in cases.ml.Gravatar herbelin2011-11-21
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
* Adding postprocessing to remove "commutative cuts" expansions inGravatar herbelin2011-11-16
* Changed the way find_dependencies_signature is working so that itGravatar herbelin2011-11-16
* De Bruijn indices bug in pattern matching compilation in the presenceGravatar herbelin2011-11-16
* Old generalization bug in pattern-matching: names were considered theGravatar herbelin2011-11-16
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
* Old typing bug in pattern-matching compilation (apparently w/oGravatar herbelin2011-11-16
* Specialization of tomatch in pattern-matching compilation was done tooGravatar herbelin2011-11-16
* A bit of documentation around cases.ml + ML modules uselessly openGravatar herbelin2011-11-16
* Fixing dependencies lifting bug in pattern-matching compilationGravatar herbelin2011-11-16
* Fixing use of type constraint for refining the "return" clause of "match".Gravatar herbelin2011-10-25
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Two bugs in pattern-matching compilation:Gravatar herbelin2011-08-08
* Cases: generic equality on constr replaced by destructorsGravatar puech2011-07-29
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 09:14:12 +0000